WTS: Let's get our hands dirty with code verification #4
Description
type: workshop
audience: intermediate
category: type-level, verification, Idris
Summary
It would be interesting to try code verifications (or proofs) hands-on after we got an introduction in #2.
This workshop could tackle the following problems:
- how do we represent data on the type-level
- what is equality / inequality
- how to proof it
It shouldn't be an introduction into the programming language Idris itself as this would take too long.