I'd love to use proofs that my software is good; but after reading the 43 page "coq in a hurry" document, I still have no idea how to prove that "print 2 + 2" prints out "4", let alone how to apply it to any of my real world apps :(
Mostly it seems formal proof stuff looks a lot like my memories of the functional programming world -- lots of one-letter variable names and unicode symbols, no code comments, any word that isn't an abbreviation is in Latin; all emphasis on the abstract, no mention of how to make this wonderful formula interact with the real world... Is there some fundamental reason that a proof language can't be as readable and practical as Python?
I presume I got downvotes for people interpreting my memories of functional programming class at university as an insult? Gah :<
But still, I would really like to know to apply formal proofs to even the simplest of real-world code bases, and the documentation that I've found on the website doesn't seem to offer that information (or if it does, it does so in a language I don't understand) -- does anyone have any links to more useful tutorials?
Mostly it seems formal proof stuff looks a lot like my memories of the functional programming world -- lots of one-letter variable names and unicode symbols, no code comments, any word that isn't an abbreviation is in Latin; all emphasis on the abstract, no mention of how to make this wonderful formula interact with the real world... Is there some fundamental reason that a proof language can't be as readable and practical as Python?