Coq is a proof assistant, which allows you to write mathematical proofs in a rigorous and formal way, and have them checked for correctness by the computer. It also allows programming with proofs of correctness for the code, and dependent types.
- - Coq is the most popular Windows, Mac & Linux alternative to Agda.
- - Coq is the most popular Open Source & free alternative to Agda.
F* is an ML-like functional programming language aimed at program verification. F* can express precise specifications for programs, including functional correctness properties. Programs written in F* can be translated to OCaml or F# for execution.
- - F* is the most popular Web-based alternative to Agda.