Implemented proofs of various (relatively) elementary mathematical results in Idris, for the Logic, Types and Spaces course at IISc.
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.