Rocq Prover AlternativesProgramming Languages and other similar apps like Rocq Prover

Alternatives list

1. 

   

   Lean Programming Language

    1 like

   Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.

   Cost / License

   • Free
   • Open Source (Apache-2.0)

   Application type

   • Programming Language

   Origin

   • United States

   Platforms

   • Visual Studio Code

   • United States

   

   

   More about Lean Programming Language  

   

   Good alternative?Is this a good alternative to Rocq Prover?

    
2. 

   

   F*

    3 likes

   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.

   Cost / License

   • Free
   • Open Source

   Application type

   • Programming Language

   Platforms

   • Mac
   • Windows
   • Linux
   • Online

   

   More about F*  

   

   Good alternative?Is F* a good alternative to Rocq Prover?

    
4. 

   

   Isabelle

    3 likes

   Isabelle is a proof assistant for writing and checking mathematical proofs by computer.

   Cost / License

   • Free
   • Open Source

   Origin

   • International

   Platforms

   • Mac
   • Windows
   • Linux

   • Global

   

   More about Isabelle  

   

   Good alternative?Is Isabelle a good alternative to Rocq Prover?

    

   |

   2comments

   ExpandCollapse

   Isabelle vs Rocq Prover Comments

   Positive comment by Guest · Feb 2, 2018

   Its logic is weaker (simply-typed HOL), but its tooling is much more developed: Prover IDE, integration of automated reasoning systems via Sledgehammer, many add-on tools, big Archive of Formal Proofs

   Positive comment by Makarius Wenzel · Feb 2, 2018

   Advanced technology and tooling.

   2 of 2 comments

   

   

   • Isabelle is Free and Open SourceRocq Prover is also Free and Open Source
5. 

   

   Agda

    2 likes

   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...

   Cost / License

   • Free
   • Open Source

   Application type

   • Programming Language

   Platforms

   • Mac
   • Windows
   • Linux

   

   Good alternative?Is Agda a good alternative to Rocq Prover?