Interactive proofs in Idris, 2019.

Implemented proofs of various (relatively) elementary mathematical results in Idris, for the Logic, Types and Spaces course at IISc.

Link to the code on Prof. Gadgil’s repository. Link to a file listing my contributions.

Positives: Some amazing hands on experience with interactive theorem proving. A funny sense of validation coming from a computer verifying a fact known to you to be trivial. My first experience with Git!

Negatives: A lot of elementary proofs were far more tedious than expected. While we expected a reasonable gap between human and computer-assisted proofs, there were (possibly never clearly stated) ways we felt Idris could be redesigned to make life easier.

Technical takeaways: Programming in a dependently typed language. Mixing algorithms for establishing elementary theorems with proofs that they work is probably a good way to set one up for program verification.

Meta takeaways: My first experience working on a large computational project. I got hands-on experience with the practice of dividing up a truly huge problem into smaller ones and tackling them separately.