Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.
United States
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 four alternatives to Isabelle for Mac, Windows, Linux, Web-based and Visual Studio Code. The best Isabelle alternative is Lean Programming Language, which is both free and Open Source. Other great apps like Isabelle are F*, Rocq Prover and Agda.
Alternatives list
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.
A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.
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...
France
EU
