Coq

Coq (hoy Rocq) es un asistente de demostración: permite escribir teoremas matemáticos y programas, y verificar formalmente que son correctos. Se ha usado para demostrar teoremas y para certificar compiladores y software crítico.

• Creado por Thierry Coquand (INRIA)
• Año 1989
• Paradigma: Funcional · asistente de pruebas
• Extensiones: .v

Para qué se usa

• Demostración de teoremas
• Verificación de software
• Investigación

A favor

• Pruebas formales fiables
• Software certificado
• Base matemática rigurosa

En contra

• Curva extrema
• Muy académico
• Lento de escribir

Ecosistema

• CoqIDE
• Gallina
• Ltac
• MathComp

Ejemplo

Require Import Coq.Strings.String.
Definition hola := "¡Hola, mundo!".