Isabelle Alternatives
Isabelle is described as 'Proof assistant for writing and checking mathematical proofs by computer' and is an app in the education & reference category. There are three alternatives to Isabelle for Mac, Windows, Linux and Web-based. The best Isabelle alternative is F*, which is both free and Open Source. Other great apps like Isabelle are Coq and Agda.
- Free • Open Source
- 6 F* alternatives
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* Features
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.
License model
- Free • Open Source
Country of Origin
- International
Platforms
- Mac
- Windows
- Linux
Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs...