Programming with Proofs – Computerphile

From Computerphile.

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:

Computerphile is a sister project to Brady Haran’s Numberphile. More at