Ask HN: How can I learn how to formally verify Haskell programs?
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?