Description #
Agda is a dependently typed functional programming language and proof assistant used for formal verification, theorem proving, and advanced type-driven development. It allows expressing mathematical proofs and programs in a unified framework.
History #
Agda originated in the early 2000s, developed by Ulf Norell and others as part of research in type theory and formal methods. It is influenced by Martin-Löf type theory and continues to evolve with a vibrant academic and formal methods community.
Hello World Code #
module HelloWorld where
open import IO.Primitive
main : IO.Unit
main = putStrLn "Hello, World!"How to Run #
Option 1: Online
Use the Agda online playground: Agda Online
Option 2: Local
- Install Agda from https://agda.readthedocs.io/en/latest/getting-started/
- Run code with:
yagda HelloWorld.agda
- Use an editor with Agda mode (Emacs, VSCode) for interactive development.
Key Concepts #
- Dependently typed: types depend on values
- Combines programming with proof writing
- Interactive development with proof checking
- Supports inductive families and higher-order functions
- Uses pattern matching and recursion extensively
- Formal verification of program correctness
- Rich standard library for mathematics and logic
- Integration with editors for proof assistance
- Strong emphasis on type safety and correctness
- Primarily used in academic and research contexts
Try It Online #
Fun Facts #
- Agda blurs the line between programming and mathematical proof.
- It is often used in research to verify algorithms and formalize mathematics.
- The language supports writing proofs that the compiler can check for correctness.
- Agda’s interactive mode helps developers construct proofs incrementally.
- It inspired other dependently typed languages like Idris.
