The Case for Formal Verification (2013)

Re:The Case for Formal Verification (2013) by Shish2k on Monday April 21, 2014 @10:51AM (#7621295)

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?

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by Shish2k on Monday April 21, 2014 @03:20PM (#7623083)

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?

[ Parent | on HN ]