Continuing our look at the Agda programming language, Professor Thorsten Altenkirch shows us how you can work with proofs, which could be invaluable in some industrial situations.
This video was filmed and edited by Sean Riley.
Computer Science at the University of Nottingham: https://bit.ly/nottscomputer
Computerphile is a sister project to Brady Haran’s Numberphile. More at http://www.bradyharan.com