DEV Community

Cover image for 🧠 Agda — The Programming Language Where Types Become Mathematical Proofs
Pʀᴀɴᴀᴠ
Pʀᴀɴᴀᴠ

Posted on

🧠 Agda — The Programming Language Where Types Become Mathematical Proofs

#programming #computerscience #learning

What is Agda?

Agda is a dependently typed functional programming language designed for writing code and mathematical proofs at the same time. Unlike normal programming languages where types simply define structure, Agda’s types can represent precise logical statements — and writing a program is equivalent to proving those statements.

Because of its expressive type system, Agda sits at the intersection of mathematics, programming, and logic — allowing you to write programs that cannot be wrong according to the type system.

Specs

Language Type: Dependently typed functional language

Released: 2007

Paradigm: Proof-driven development, functional, total programming

Execution Model: Interactive editor + compiled execution

Typing: Dependent, expressive, mathematically rigorous

Example Code (Tiny Proof + Output) 

module Hello where

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not true  = false
not false = true
Enter fullscreen mode Exit fullscreen mode

A basic theorem:

not-involutive : (b : Bool) → not (not b) ≡ b
not-involutive true  = refl
not-involutive false = refl
Enter fullscreen mode Exit fullscreen mode

This proves: applying not twice gives the same value.

How It Works

Agda programs combine:

  • Types
  • Definitions
  • Proofs
  • Functions
  • Equations

The programmer writes code interactively using editor-assisted refinement. Errors mean the proof isn’t yet complete. The system ensures:

  • No infinite recursion (totality)
  • No unhandled logic cases
  • No undefined behavior
  • No wrong assumptions

Agda also supports pattern matching, inductive types, Unicode identifiers, and interactive theorem refinement.

Strengths

  • Extremely expressive type system
  • Guarantees correctness by construction
  • Used in formal verification and advanced computer science research
  • Models mathematical objects, logic, and proofs cleanly

Weaknesses

  • Hard to learn without math or type theory background
  • Software development is slower than typical languages
  • Tooling and ecosystem are academic rather than industrial
  • Syntax and workflow feel unusual to most developers

Where to Run

Agda can be used with:

  • Emacs mode (best experience)
  • VS Code + Agda extension
  • Command-line compiler
  • Online Agda playgrounds

Interactive proof mode is the core workflow.

Should You Learn It?

  • For normal coding: No
  • For proof engineering, formal methods, or advanced CS: Yes
  • For hobby exploration of logic and type theory: Highly interesting
  • For building apps fast: Not ideal

Summary

Agda is not just a programming language — it’s a framework for proving the correctness of programs using types as mathematical statements. While niche and intellectually demanding, Agda represents one of the most powerful ideas in modern computer science: software that is mathematically guaranteed to be correct rather than merely tested.

Top comments (0)