title: Can Haskell functions be proved/model-checked/verified with correctness properties?
body: <p>Continuing on from ideas in: <a href="https://stackoverflow.com/questions/4065001/are-there-any-provable-real-world-languages-scala">Are there any provable real-world languages?</a></p>
  
  <p>I don't know about you, but I'm <strong>sick of writing code that I can't guarantee.</strong></p>
  
  <p>After asking the above question and getting a phenomenal response (Thanks all!) I have decided to narrow my search for a provable, pragmatic, approach to <a href="http://www.haskell.org/" rel="noreferrer">Haskell</a>. I chose Haskell because it is actually useful (there are <a href="http://snapframework.com/" rel="noreferrer">many</a> <a href="http://happstack.com/" rel="noreferrer">web</a> <a href="http://www.turbinado.org/" rel="noreferrer">frameworks</a> written for it, this seems a good benchmark) <strong>AND</strong> I think it is strict enough, <a href="http://en.wikipedia.org/wiki/Functional_programming" rel="noreferrer">functionally</a>, that it might be provable, or at least allow the testing of invariants.</p>
  
  <p><strong>Here's what I want</strong> (and have been unable to find)</p>
  
  <p>I want a framework that can look at a Haskell function, add, written in psudocode:</p>
  
  <pre><code>add(a, b):
      return a + b
  </code></pre>
  
  <p>- and check if certain invarients hold over every execution state. I'd prefer for some formal proof, however I would settle for something like a model-checker.<br>
  In this example, the invarient would be that given values <em>a</em> and <em>b</em>, the return value is always the sum <em>a+b</em>.</p>
  
  <p>This is a simple example, but I don't think it is an impossibility for a framework like this to exist. There certainly would be an upper limit on the complexity of a function that could be tested (10 string inputs to a function would certainly take a long time!) but this would encourage more careful design of functions, and is no different than using other formal methods. Imagine using Z or B, when you define variables/sets, you make damn sure that you give the variables the smallest possible ranges. If your INT is never going to be above 100, make sure you initialise it as such! Techniques like these, and proper problem decomposition should - I think - allow for satisfactory checking of a pure-functional language like Haskell.</p>
  
  <p>I am not - yet - very experienced with formal methods or Haskell. Let me know if my idea is a sound one, or maybe you think that haskell is not suited? If you suggest a different language, please make sure it passes the "has-a-web-framework" test, and do read the original <a href="https://stackoverflow.com/questions/4065001/are-there-any-provable-real-world-languages-scala">question</a> :-)</p>