Gallina

A Functional programming language (Rocq's specification language) that allows writing purely functional programs and formal proofs, using Dependent type to express precise logical properties.