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.
https://www.facebook.com/computerphile
https://twitter.com/computer_phile
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
