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

**Utilize the capacity of the computers in a reliable way.**

Targets:

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

**Elimination of errors**- no runtime errors

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

- no runtime errors
**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

- programming with types as data (generic programming, universes)

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.

Additional features

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

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

- most Haskell type system extensions are just special cases
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

- type theory