Ask HN: How can I learn how to formally verify Haskell programs?

2 pointsby modmajgen16 anni fa1 comments

To give some context into my current state of knowledge, I'm currently enrolled in a calculus course. My experience with formal logic is somewhat limited, but I have played around with both propositional and predicate calculus.

As of late, I've been extremely obsessed with the idea of formal correctness. Even though it's fairly unlikely that I'll be more employable with the skill, I'm still curious on how to learn formal verification, if only for the fact that it'll help me reason with existing programs better and the confidence of having a 100% correct algorithm is pretty cool :)

Unfortunately, searches on the Haskell wiki and on Google give me links to research papers that I unfortunately don't have the prerequisites to understand. A Wikipedia search explains that through the Curry-Howard Isomorphism allows for programs to be translated into combinatory logic and then be reasoned with, but I'm not sure whether simple combinatory logic is enough to handle a language like Haskell.

So, if I'm going to approach the beast, what would be the best way to do so? What kind of knowledge should I know about logic and Haskell, and what kind of books or articles would best explain the required concepts?

1 comments

KevinMS16 anni fa

This stuff is over my head, and I might be stating the obvious to you, or this might be useless for Haskell, but because you didn't mention it explicitly:

http://en.wikipedia.org/wiki/Cleanroom_Software_Engineering

http://www.amazon.com/Cleanroom-Software-Engineering-Technol...