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.
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.