Rocquencourt的构造演算原型
1980年代初，蒂埃里·科康与热拉尔·于埃在法国国家信息与自动化研究所INRIA的Rocquencourt研究中心探索数学证明的机械化。1984年开始实现的原型，以构造演算为逻辑基础，用ML家族语言编写。早期系统曾称CONSTR或CoC，后来才逐渐采用Coq这一名称。
1985年两人的论文给出在原型上发展的数学例子。用户写下的不是一段只供人阅读的论证说明，而是由系统解析、赋予类型并检查的表达式。原型把命题、数学对象与证明置于同一个形式语言中，使理论规则成为可执行检查程序的依据。
一个恒等函数也是一个证明
1985年论文先定义命题A推出A，再用恒等函数给出证明。其核心写成“[u:A]u”：输入一个类型为A的对象u，原样返回u；论文还把它包装为对任意A都适用的Id。若A表示命题，u便可理解为A的一个证明，返回u就实现了从A得到A。
这个小例子说明了命题与类型、证明与程序之间的对应。检查器要验证变量处在允许的上下文中，函数输入与输出的类型也必须合适。复杂证明则把这样的构造逐层组合。计算机检查的是明确的形式表达式，使用者仍须决定所陈述的命题是否准确表达了原来的数学问题。
从直接写对象到逐步处理目标
直接写出完整证明对象很容易变得繁琐。早期系统发展了数学叙述语言，允许声明公理、参数和定义；吉勒·多韦克参与建立章节机制，使一组带有局部假设的结果能够组织起来。到4系列，数学文件可与实现用的ML源文件分开保存，研究者不必把所有操作都混在工具程序内部。
交互证明器又允许从目标向下分解子目标，使用以CAML编写的策略尝试推理。策略可以帮助寻找证明，却不直接成为最终保证：完整证明项生成后，构造引擎还要重新检查。官方历史记录甚至提到，早期用户会遇到搜索似已成功、最终却因类型层级不一致而检查失败的情况。
参考：[2]
1989年的发布究竟指什么
官方早期版本史将稳定4.10版的发布日期记为1989年5月1日，它随CAML 2.6分发，并有于埃、科康及多韦克分别编写的引擎、策略和叙述语言文档。此前已有冻结版本和早期用户，例如4.3版在1987年末曾向小范围社群分发。因此，1989年的公开系统并非从零突然出现。
同年，科康与克里斯蒂娜·波兰—莫林研究把原生归纳类型加入构造演算，使自然数、列表等对象及其归纳证明更便于表达。1989年末开始5.1版的工作，1991年发布5.6版。1989年公开4.10版与1991年新基础系统的发布，不应合并成一个日期或一个完全相同的版本。
证明中的计算内容
原始构造演算可以用函数编码一些归纳对象，但写法和运算都不够便利。归纳类型扩展以及相应策略，为更直接地定义数据和按其结构证明性质提供条件。波兰—莫林还推进从构造性证明中提取程序的算法，布鲁诺·韦尔纳参与把提取出的项编译为实际函数式程序的工具。
这种方法把规格与证明联系起来：使用者区分需要保留的计算对象和描述其性质的逻辑内容，再从合适的证明中得到程序。它并非任何自然语言论证都能自动转换的软件工厂。后来团队不断改进实现、库与接口，项目今天称为Rocq；理解其早期形成，仍须把最初检查器、交互工作方式和后来的程序提取分别放回各自版本。