Walter has worked and studied in South Africa, Amsterdam and London using languages such as Coq, Go, Haskell, Erlang and Elm.
He spends his free time doing a phd as a hobby, pair programming in Coq and competing with potatoes on couches.
In this talk we will give introduction to the possibilities of writing code that is verified using proofs.
The scene is a dialog between the developer and the (dependent) typechecker demonstrated as a dialog between the two speakers.
The talk will illustrate how the typechecker can aid the developer to write correct programs using proofs. We will demo the basics with examples from Boolean logic and recursive functions using induction. We will talk about how this is used in practice in browser security and smart contracts.