최근 수정 시각 : 2025-07-06 00:40:00

Rocq

Coq에서 넘어옴

[[프로그래밍 언어|'''프로그래밍 언어
{{{#!wiki style="font-family: Times New Roman, serif; display: inline;"]]
{{{#!wiki style="min-height: calc(1.5em + 5px); margin: 0 -10px -5px"
{{{#!wiki style="display: inline-table; min-width: 40%; min-height: calc(1.5em + 5px)"
{{{#!folding [ 목록 ]
{{{#!wiki style="margin: -5px -1px"		<colbgcolor=royalblue><colcolor=#fff> ※ 나무위키에 등재된 프로그래밍 언어 목록
AActionScript · AdaT · AgdaTP · ALGOLT · ApexT · APL · awk · AssemblyT
BBASIC
C파일:C언어 로고.svg CT · 파일:C C#T · 파일:C++ 로고.svg C++T · CarbonT · 파일:clojure_logo.png ClojureS · COBOLT · CoffeeScript · Common LispS · CrystalT
D파일:external/upload.wikimedia.org/D_programming_language_logo.png DT · 파일:Dart 심볼.svg DartT
EElixir · 파일:Elm_logo.svg.png elmT · Erlang
F파일:fsharp-logo.png F#T · Factor · 파일:fennel-logo.svg FennelS · 파일:forth.png Forth · FortranT
GGNU Octave · 파일:Go 로고.svg GoT · Groovy
H파일:Haskell 로고 심볼.svg HaskellT · HolyCT · Haxe
I
J파일:Java 로고.svg JavaT · 파일:JavaScript 로고.svg JavaScript · 파일:julia-dots.svg Julia
K파일:Kotlin 심볼.svg KotlinT
LLeanTP · 파일:LISP_logo.svg LISPS · 파일:Lua 로고.svg Lua
MMATLAB · MaxV · MojoT · Moonlight
N파일:Nim 왕관 로고.svg NimT · 파일:Nix 로고.svg Nix
OOberonT · Objective-CT · 파일:ocaml.svg OCamlT
PPascalT · Perl · 파일:PHP 로고.svg PHP · Processing · Prolog · 파일:Python 심볼.svg Python
QQ#T · QML
R파일:R 로고.svg R · 파일:racket-logo.svg RacketS · Raku · ReasonMLT · 파일:rocq.png RocqTP · 파일:Ruby 로고.svg Ruby · 파일:Rust 로고.svg파일:Rust 로고 화이트.svg RustT
SSAS · 파일:Scala 로고.png ScalaT · SchemeS · 파일:스크래치(교육 플랫폼) 로고.svg ScratchV · sed · Shell Script · Smalltalk · SQL · 파일:Swift 심볼 배경.svg SwiftT
T파일:Typescript_logo_2020.svg TypeScriptT
UUdon
VVisual Basic · Visual Basic .NET · Visual Basic for Applications · vvvvV
WWave
XXSharp
Y
ZZenScript · 파일:Zig 로고마크.svg ZigT
한글누리 · 숨V · 씨앗 · 약속 · 파일:엔트리 아이콘.svg 엔트리V · 창조
T: 정적 타입 프로그래밍 언어 · P: 증명 보조 언어 · S: LISP 방언 및 S-표현식 기반 언어 · V: 시각적 프로그래밍 언어 }}}}}}}}}{{{#!wiki style="display: inline-table; min-width: 40%; min-height: calc(1.5em + 5px)"
{{{#!folding [ 순위 ]
{{{#!wiki style="margin: -5px -1px -10px"		 {{{#!wiki style="min-height: calc(1.5em + 5px); margin: 0 -10px -5px"
{{{#!wiki style="display: inline-table; min-width: 25%; min-height: calc(1.5em + 5px)"
{{{#!folding [ IEEE Spectrum 2025 ]
{{{#!wiki style="margin: -5px -1px"		<tablewidth=100%><tablebgcolor=transparent><colbgcolor=#11a500><colcolor=#fff> 스펙트럼 부문 상위 10개 프로그래밍 언어 <colbgcolor=#ff1100><colcolor=#fff> 직업 부문 상위 10개 프로그래밍 언어
1 Python 1 Python
2 Java 2 SQL
3 C++ 3 Java
4 SQL 4 JavaScript
5 C# 5 TypeScript
6 JavaScript 6 C#
7 TypeScript 7 C++
8 C 8 HTML
9 Shell 9 Go
10 Go 10 Shell }}}}}}}}}{{{#!wiki style="display: inline-table; min-width: 25%; min-height: calc(1.5em + 5px)"
{{{#!folding [ Stack Overflow 2025 ]
{{{#!wiki style="margin: -5px -1px"		<colbgcolor=#ffa500><colcolor=#fff> 2025년 Stackoverflow 설문조사 상위 25개 프로그래밍 언어
1 JavaScript <colbgcolor=#ffa500><colcolor=#fff> 14 Rust
2 HTML & CSS 15 Kotlin
3 SQL 16 Lua
4 Python 17 어셈블리어
5 Bash/Shell 18 Ruby
6 TypeScript 19 Dart
7 Java 20 Swift
8 C# 21 R
9 C++ 22 Groovy
10 PowerShell 23 Visual Basic
11 C 24 VBA
12 PHP 25 MATLAB
13 Go }}}}}}}}}{{{#!wiki style="display: inline-table; min-width: 25%; min-height: calc(1.5em + 5px)"
{{{#!folding [ TIOBE 2025 ]
{{{#!wiki style="margin: -5px -1px"		<colbgcolor=#2777c2><colcolor=#fff> 2025년 10월 TIOBE 검색어 점유율 상위 20개 프로그래밍 언어
1 Python <colbgcolor=#2777c2><colcolor=#fff> 11 Fortran
2 C 12 Perl
3 C++ 13 R
4 Java 14 PHP
5 C# 15 Assembly language
6 JavaScript 16 Rust
7 Visual Basic 17 MATLAB
8 Go 18 Scratch
9 Delphi / Object Pascal 19 Ada
10 SQL 20 Kotlin }}}}}}}}}{{{#!wiki style="display: inline-table; min-width: 25%; min-height: calc(1.5em + 5px)"
{{{#!folding [ PYPL 2025 ]
{{{#!wiki style="margin: -5px -1px -10px"		<colbgcolor=green><colcolor=#fff> 2025년 11월 PYPL 검색어 점유율 상위 20개 프로그래밍 언어
1 Python <colbgcolor=green><colcolor=#fff> 11 Ada
2 Java 12 TypeScript
3 C++ 13 MATLAB
4 Objective-C 14 Kotlin
5 R 15 PowerShell
6 JavaScript 16 Go
7 C# 17 Dart
8 Swift 18 Ruby
9 PHP 19 Lua
10 Rust 20 VBA }}}}}}}}}}}} }}}}}}}}}}}}
실행 방식 · 분류 · 언어 목록(분류:프로그래밍 언어 문법) · 언어별 예제 · 틀:프로그래밍 언어 문법 · 틀:난해한 프로그래밍 언어

이 문서는 토막글입니다.

토막글 규정을 유의하시기 바랍니다.


1. 개요2. 외부 링크

1. 개요

Rocq는 CIC(Calculus of Inductive Constructions)에 기반한 증명보조기이다. OCaml과 마찬가지로 프랑스의 Inria에서 개발되었다. 구현은 OCaml로 되어있으며, Rocq 코드를 OCaml이나 Haskell로 추출하여 프로그래밍 언어로도 사용할 수 있다.

Rocq의 과거 명칭인 Coq이라는 단어는 프랑스어로 수탉이라는 뜻이 있으며, 동시에 Coq의 기반 이론인 CoC(Calculus of Constructions)와 CoC의 개발자중 한명인 Thierry Coquand 등을 중의적으로 의미한다. 한편 Coq과 영어권 은어 cock의 발음 유사성 때문에[1] Coq을 Rocq로 개명하는 제안이 받아들여졌으며, 현재 추진 중이다.[2]

2. 외부 링크

[1] 프랑스어로 coq은 발음이 명확히 다르기 때문에 프랑스어 화자 입장에서는 억울할 수 있는 부분이다. Coq은 프랑스의 국립 연구소인 Inria에서 개발 했기 때문에 프랑스인의 기여가 큰 편이다.[2] Change of name: Coq -> The Rocq Prover

분류