About the tutorial
Goals
- show what is Agda 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
More about the tutorial
What is Agda good for?
To utilize the capacity of computers in a reliable way.
Target:
programming and mathematics;
formal definitions, theorems, proofs and algorithms
Benefits of programming in Agda
- eliminating 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 list, balanced tree 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, ...
- safe optimization
- runtime checks like array index bounds checks are eliminated
- defensive coding (generous on input, strict on output) is unnecessary -- 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)
Type may depend on runtime value and still checked in compile time.
- reflection
- Previously unseen range of embedded domain specific languages can be defined with arbitrary precision.
Definitions
- classical, constructive and modal logical connectives are definable
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.
In this way algorithms can be used during proofs.
- automatic proof checking
Additional features
- inferred terms, implicit arguments
- holes, interactive development
- unicode characters, mixfix operators
Benefits of completing the tutorial
- use Agda directly (you have to put more effort in learning Agda for this)
- develop formal systems, use Agda during 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 theory easier (will be more familiar for you)
- type theory
- constructive mathematics
- semantics of programming languages