Correct Code by Construction

Programming Languages
Voting no longer possible
Voting enabled when talk has started

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.

Walter Schulze


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.

Paul Cadman

Paul is a mathematician and software engineer with a PhD in algebraic geometry from the University of Warwick. He has worked on mobile applications for retail banking, collaborated with scientists from the Alan Turing Institute to implement a proximity exposure algorithm for the NHS England COVID-19 app, and worked on a computational law decision engine for global financial regulations. He is an enthusiast for the use of formal methods to improve the quality of software systems and in 2018 founded the Type Driven Development study group which focuses on certified programming and formalization of mathematics.