Agda AlternativesProgramming Languages and other similar apps like Agda

Agda is described as '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' and is a programming language in the development category. There are four alternatives to Agda for Mac, Windows, Linux, Web-based and Visual Studio Code. The best Agda alternative is Lean Prover, which is both free and Open Source. Other great apps like Agda are F*, Rocq Prover and Isabelle.

More about Agda
Copy a direct link to this comment to your clipboard
Agda alternatives page was last updated

Alternatives list

  1. Lean Prover icon

    Lean Prover

     1 like

    Lean is a functional programming language and interactive theorem prover based on dependent type theory. Dependent type theory unites the worlds of programs and proofs; thus, Lean is also a programming language.

    Cost / License

    Application type

    Platforms

    • Mac
    • Windows
    • Linux
    • Visual Studio Code
     

    • Lean Prover is the most popular Windows, Mac & Linux alternative to Agda.

    • Lean Prover is the most popular Open Source & free alternative to Agda.

    • Lean Prover is Free and Open SourceAgda is also Free and Open Source
  2. F* icon

    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

    Platforms

    • Mac
    • Windows
    • Linux
    • Online
    F* screenshot 1
     

    • F* is the most popular Web-based alternative to Agda.

    • F* is Free and Open SourceAgda is also Free and Open Source
  4. Rocq Prover icon

    Rocq Prover

     4 likes

    A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.

    Cost / License

    Application type

    Platforms

    • Mac
    • Windows
    • Linux
    Rocq's highly expressive type system and proof language enable fully mechanised verification of programs with respect to strong specifications in a wide variety of languages.
     
  5. Isabelle icon

    Isabelle

     3 likes

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

    Cost / License

    • Free
    • Open Source

    Platforms

    • Mac
    • Windows
    • Linux
    Isabelle screenshot 1
     
4 of 4 Agda alternatives