Agda

Agda is a dependently typed functional programming language and interactive proof assistant. Built on Intuitionistic Type Theory, Agda allows writing mathematical proofs alongside programs, providing formal verification and strong static type guarantees.

Installation

Install Agda and its standard library on Ubuntu:

apt update
apt install -y agda agda-stdlib

Verification

Check the installed version of Agda:

agda --version

Writing and Compiling Code

Create an Agda source file named Hello.agda:

module Hello where

open import IO

main : Main
main = run (putStrLn "Hello, World!")

Compile the code into an executable binary using the GHC backend:

agda --compile Hello.agda

Run the compiled executable:

./Hello

Official Resources

• Official Website