Goals

• Show what Agda is good for
• Teach Agda syntax and semantics
• Teach Agda programming skills

Features

• Slides: 1/3 examples, 1/3 explanation, 1/3 exercises
• Only (part of) secondary school mathematics is required

# What is Agda good for?

Utilize the capacity of the computers in a reliable way.

Targets:

• Joining programming and mathematics
• Formal definitions, theorems, proofs, and algorithms

# Benefits of programming in Agda

• Elimination of errors

• no runtime errors
Inevitable errors like I/O errors are handled, others are excluded by design.
• no non-productive infinite loops
• Machine-checked documentation

• any functional properties can be formalized and proved -- proof checking is automatic
• distinction between finite and infinite data like lists vs. streams
• invariant properties of data like sorted lists and balanced trees can be maintained
• function properties like commutativity, associativity can be maintained
• Exact interfaces

Formal specification can be given with the help of exact mathematical concepts like groups, rings, lattices, categories, and so on.

• Safe optimization

• runtime checks like array bounds checks are eliminated
• defensive coding (generous on input, strict on output) is unnecessary -- there is no overhead of it
• safe optimization on special input like associative input function of a higher-order function
• High-level programming

• programming with types as data (generic programming, universes)
Types may depend on values in run time and still checked in compile time.
• reflection
• previously unseen range of embedded domain-specific languages can be defined with arbitrary precision

# Benefits of creating formal systems in Agda

Definitions

• Classical, constructive, and modal logical connectives can be defined.

Theorems

• One can quantify over elements, properties, properties of properties etc.
(Agda has the strength of an infinite-order logic.)

Proofs

• Automatic simplification of expressions gives the automatic part of proofs.
This way algorithms can be used in proofs.
• Automatic proof checking.

• Inferred terms, implicit arguments.
• Holes, interactive development.
• Unicode characters, mixfix operators.

# Benefits of completing this tutorial

After completing this tutorial, you will be able to:

• Use Agda directly (you have to put more effort in learning Agda for this)

• develop formal systems, use Agda in research
• write high-assurance code
Note that the current compiler is not industrial-strength, libraries are missing,
solutions for individual problems are not worked out.
• Learn similar languages easier

• most Haskell type system extensions are just special cases
• Haskell is a practical general-purpose programming language also used in industry.
• languages with similar goals: Coq, Idris, Epigram
• write formal proofs in Coq which is more mainstream
• Use the ideas presented here

• have a better programming style / understanding in other languages
• steal the ideas
• Learn related theoretical concepts easier (which will be more familiar for you)

• type theory
• dependent types
• constructive mathematics
• semantics of programming languages
• λ-calculus