I don't like mechanized proofs anymore, friendship ended with proof code
It's cool that I can dump entire proofs into a proof checker, but it's entirely unenlightening
I'm spending massive amounts of time being a proof gremlin and doing inverts and associativities and whiskering and other minor tasks compared to the actual body of the proof
The aesthetics of an elegant textual explanation of a sequential proof is utterly destroyed by all the ugly details
This is not a place of honour, nothing valued is here
Programming with dependent types is cool though, I think we should do more of that
Maybe I only say this because I haven't yet tackled any significantly large development using Idris
One day I'll be frustrated by all the issues from overly dependent program code and be like friendship ended with types. Racket is my new best friend
I'm thinking the difficulty with proving things using proof assistants might also be a user interface issue and not just a technical issue with the proof assistant not being smart enough
I might learn something useful from that HCI class... if I hadn't dropped it lmao
@ionathanch There are technical issues behind the HCI issues though. Equality is too hard to work with in proof assistants. It's too hard to convince proof assistants that things are equal (as opposed to convincing humans in paper proofs). I'm not sure we can overcome this with HCI improvements.
