Coq facts for kids
 |
|
| Developer(s) | The Coq development team |
|---|---|
| Initial release | 1 May 1989 (version 4.10) |
| Written in | OCaml |
| Operating system | Cross-platform |
| Available in | English |
| Type | Proof assistant |
| License | LGPLv2.1 |
Coq is a special computer program that helps people check if mathematical proofs are correct. It was first released in 1989. Think of it like a super-smart math teacher who can check every step of a proof.
Coq lets you write down mathematical ideas. Then, it can automatically check if your proofs for these ideas are true. It even helps you find the right steps to prove things. Coq can also turn a proven idea into a working computer program.
This software uses a special math system called the calculus of inductive constructions. While Coq isn't fully automatic, it has tools that can help solve parts of a proof on their own.
Many smart people were honored for creating Coq. The Association for Computing Machinery gave the 2013 ACM Software System Award to Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, and others for their work on Coq.
The name "Coq" is a fun play on words. It comes from Thierry Coquand's name. It also sounds like "CoC," which stands for "Calculus of Constructions." Plus, "coq" means "rooster" in French, following a tradition of naming computer tools after animals.
Contents
What is Coq Software?
Coq can be seen in two ways. First, it's a type of programming language. This language is designed to be very precise and ensures that programs always finish running. Second, Coq is a logic system. This means it's a way to organize and check complex mathematical ideas.
Who Developed Coq?
The development of Coq started in 1984. It has been supported by INRIA, a French research institute. Other universities and research centers also help. These include École Polytechnique and University of Paris-Sud.
The project was started by Gérard Huet and Thierry Coquand. Over 40 researchers have added features to Coq. The main team leaders have changed over the years. Coq is mostly built using another programming language called OCaml. It can also be expanded with special add-ons called plugins.
Why is it Called Coq?
The name coq means "rooster" in French. This name follows a French tradition. Researchers often name their computer tools after animals.
Before 1991, the program was called "CoC." This stood for "Calculus of Constructions." In 1991, a new version was made. It was based on an improved system called the Calculus of Inductive Constructions. That's when the name changed to Coq. It was a nod to Thierry Coquand, who helped create the original Calculus of Constructions.
What is Gallina?
Coq uses a special language for writing down ideas. This language is called Gallina. "Gallina" means "hen" in Latin and other languages.
Programs written in Gallina have a cool feature: they always finish running. This is important because some computer programs can get stuck in endless loops. Gallina avoids this problem. It helps make sure that the proofs and programs created with Coq are reliable.
Four Color Theorem and SSReflect
In 2002, two researchers, Georges Gonthier and Benjamin Werner, used Coq. They created a clear proof for the four color theorem. This theorem states that any map can be colored with only four colors. No two areas next to each other will have the same color.
Their work led to a big improvement for Coq. They developed something called SSReflect. This stands for "Small Scale Reflection." Even though it has a specific name, many of its features are useful for all kinds of proofs.
What Does SSReflect Do?
SSReflect added many helpful tools to Coq. These tools make it easier to write and check proofs. Some of these features include:
- Easier Matching: Better ways to find specific patterns in your code.
- Hidden Arguments: Functions can sometimes guess missing information.
- Short Arguments: A quicker way to write down simple inputs.
- Improved Tactics: A more powerful "set" command for proofs.
- Reflection Support: Helps the program think about its own rules.
SSReflect 1.11 is free to use. It works with Coq 8.11.
How Coq is Used
Coq is used in many important computer science projects. Here are a few examples:
- CompCert: This is a special C programming language compiler. A compiler turns code you write into something a computer understands. CompCert is largely built and proven correct using Coq. This means it's super reliable.
- Disjoint-set data structure: This is a way to organize data in computer programs. In 2007, a proof that it works correctly was published using Coq.
- Feit–Thompson theorem: This is a very complex math theorem. A formal proof of it using Coq was finished in 2012.
- Four color theorem: As mentioned before, a formal proof of this map-coloring theorem was completed with Coq in 2005.
See also
In Spanish: Coq para niños
