Can Haskell functions be proved/model-checked/verified with correctness properties?

Question

Continuing on from ideas in: Are there any provable real-world languages?

I don't know about you, but I'm sick of writing code that I can't guarantee.

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 Haskell. I chose Haskell because it is actually useful (there are many web frameworks written for it, this seems a good benchmark) AND I think it is strict enough, functionally, that it might be provable, or at least allow the testing of invariants.

Here's what I want (and have been unable to find)

I want a framework that can look at a Haskell function, add, written in psudocode:

add(a, b):
    return a + b

- 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.
In this example, the invarient would be that given values a and b, the return value is always the sum a+b.

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.

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 question :-)

Solution 1

Well, a few things to start with, since you're taking the Haskell route:

• Are you familiar with the Curry-Howard correspondence? There are systems used for machine-checked proofs based on this which are, in many ways, simply functional programming languages with very powerful type systems.

• Are you familiar with the areas of abstract mathematics that provide useful concepts for analyzing Haskell code? Various flavors of algebra and some bits of category theory come up a lot.

• Keep in mind that Haskell, like all Turing-complete languages, always has the possibility of nontermination. In general, it's much harder to prove that something will always be true than it is to prove that either something will be true or will depend on a nonterminating value.

If you're seriously going for proof, not merely testing, these are the sort of things to keep in mind. The basic rule is this: Make invalid states cause compiler errors. Prevent invalid data from being encoded in the first place, then let the type checker do the tedious part for you.

If you want to go even further, if memory serves me the proof assistant Coq has an "extract to Haskell" feature that will let you prove arbitrary properties about critical functions, then turn the proofs into Haskell code.

For doing fancy type system stuff directly in Haskell, Oleg Kiselyov is the Grand Master. You can find examples on his site of neat tricks like higher-rank polymorphic types to encode static proofs of array bounds checking.

For more lightweight stuff, you can do things like using a type-level certificate to mark a piece of data as having been checked for correctness. You're still on your own for the correctness check itself, but other code can at least rely on knowing that some data has, in fact, been checked.

Another step you can take, building off of lightweight verification and fancy type system tricks, is to use the fact that Haskell works well as a host language for embedding domain-specific languages; first construct a carefully restricted sublanguage (ideally, one that isn't Turing-complete) about which you can more easily prove useful properties, then use programs in that DSL to provide key pieces of core functionality in your overall program. For instance, you could prove that a two-argument function is associative in order to justify parallelized reduction of a collection of items using that function (since the ordering of function application doesn't matter, only the ordering of arguments).

---

Oh, one last thing. Some advice on avoiding the pitfalls that Haskell does contain, which can sabotage code that would otherwise be safe-by-construction: Your sworn enemies here are general recursion, the IO monad, and partial functions:

• The last is relatively easy to avoid: Don't write them, and don't use them. Make sure that every set of pattern matches handles every possible case, and never use error or undefined. The only tricky part is avoiding standard library functions that may cause errors. Some are obviously unsafe, like fromJust :: Maybe a -> a or head :: [a] -> a but others may be more subtle. If you find yourself writing a function that really, truly cannot do anything with some input values, then you're allowing invalid states to be encoded by the input type and need to fix that, first.

• The second is easy to avoid on a superficial level by scattering stuff through assorted pure functions that are then used from an IO expression. Better is to, as much as possible, move the entire program out into pure code so that it can be evaluated independently with everything but the actual I/O. This mostly becomes tricky only when you need recursion that's driven by external input, which brings me to the final item:

• Words to the wise: Well-founded recursion and productive corecursion. Always ensure that recursive functions are either going from some starting point to a known base case, or are generating a series of elements on demand. In pure code, the easiest way to do this is by either recursively collapsing a finite data structure (e.g., instead of a function calling itself directly while incrementing a counter up to some maximum, create a list holding the range of counter values and fold it) or recursively generating a lazy data structure (e.g. a list of progressive approximations to some value), while carefully never mixing the two directly (e.g., don't just "find the first element in the stream meeting some condition"; it might not exist. Instead, take values from the stream up to some maximum depth, then search the finite list, handling the not-found case appropriately).

• Combining the last two items, for the parts where you really do need IO with general recursion, try to build the program as incremental components, then condense all the awkward bits into a single "driver" function. For instance, you could write a GUI event loop with a pure function like mainLoop :: UIState -> Events -> UIState, an exit test like quitMessage :: Events -> Bool, a function to get pending events getEvents :: IO Events, and an update function updateUI :: UIState -> IO (), then actually run the thing with a generalized function like runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO (). This keeps the complicated parts truly pure, letting you run the whole program with an event script and check the resulting UI state, while isolating the awkward recursive I/O parts into a single, abstract function that's easy to comprehend and will often be inevitably correct by parametricity.

Solution 2

Probably the closest thing to what you're asking for is Haskabelle, a tool that comes with the proof assistant Isabelle which can translate Haskell files into Isabelle theories and lets you prove stuff about them. As far as I understand this tool is developed within the HOL - ML - Haskell project and the documentation page contains some information about the theory behind.

I'm not terribly familiar with this project and I don't know very much about what has been done with it. But I know Brian Huffman has been playing around with these things, check out his papers and talks, they should contain relevant stuff.

Solution 3

I'm not sure whether what you ask for is actually what will make you happy. :-)

Model-checking a general purpose language is neigh impossible since models must be domain specific to be practical. Due to Gödel's Incompleteness Theorem, there simply is no method for automatically finding proofs in a sufficiently expressive logic.

This means that you have to write proofs yourself, which raises the question of whether the effort is worth the time spent. Of course, the effort creates something very valuable, namely the assurance that your program is correct. The question is not whether this is a must-have, but whether the time spent is too great a cost. The thing about proofs is that while you may have an "intuitive" understanding that your program is correct, it is often very difficult to formalize this understanding as a proof. The problem with intuitive understanding is that it's highly susceptible to accidental mistakes (typos and other stupid mistakes). This is the basic dilemma of writing correct programs.

So, research about program correctness is all about making it easier to formalize proofs and to check their correctness automatically. The programming is an integral part of the "ease of formalization"; it is very important to write programs in a style that is easy to reason about. Currently, we have the following spectrum:

• Imperative language like C, C++, Fortran, Python: Very difficult to formalize anything here. Unit tests and general reasoning are the only way to get at least some assurance. Static typing catches only trivial bugs (which much better than not catching them!).

• Purely functional languages like Haskell, ML: Expressive type system helps catch non-trivial bugs and mistakes. Proving correctness by hand is practical for snippets of up to somewhere around 200 lines, I'd say. (I did a proof for my operational package, for instance.) Quickcheck testing is a cheap substitute for formalized proofs.

• Dependently typed languages and proof assistants like Agda, Epigram, Coq: Proving whole programs correct is possible thanks to automated help with proof formalization and discovery. However, the burden is still high.

In my opinion, the current sweet spot for writing correct programs is purely functional programming. If lives depend on the correctness of your program, you better go a level higher and use a proof assistant.

Solution 4

Sounds like you want ESC/Haskell: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm

Oh, and Agda now does have a web framework (proof of concept, at least): http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/

Solution 5

Have you had a look at quickcheck? It may offer some of the things you need.

http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck

View more solutions

Comments

[C. A. McCann]

@Steven: Really? Why would that be the case? If a piece of code has been proven to have some property, it will always have that property no matter what other code it interacts with, and you can rely on that property in other proofs. Proofs are reusable and compositional in a way that tests aren't, and by encoding proofs in the type system there's no chance of them getting out of sync with the code itself.

[0atman]

@Steven: Yeah, I agree with camccann, I don't have to test each combination of bricks in a house. Nice goat though!

[C. A. McCann]

@Steven: They don't have to, that's the whole point! If a function is provably correct for all possible inputs, then the only obligation necessary to use it is providing arguments of the appropriate type. Not having to worry about points of integration is exactly why type-encoded proofs are compositional. Knowing that a chunk of code is guaranteed to never fail or produce runtime errors is why static typing is nice.

[C. A. McCann]

@Steven: Personally I'd rather spend a bit longer to write code that can't break instead of writing unreliable code and then wasting time writing trivial tests and worrying about everything that could go wrong... but to each their own, I suppose!

[0atman]

Thanks for your views guys, take it to a forum :-)

[Fred Foo]

I'd like to add that I at least felt like a mechanical theorem prover at the exam ;)

[0atman]

Yes, I think it looks fantastic, and definitely would be the basis for further research for me.

[0atman]

Thanks, do you think it is possible to model-check Haskell directly?

[0atman]

ESC/Haskell looks good, though the implementation is theoretical and a little limited, based on my skim through the paper. A great resource, however - thank you!

[C. A. McCann]

@Oatman: In the general case, just as much as it is possible to model-check any programming language. Many of the techniques that might be used to reduce or simplify the state space to examine are easy or automatic in Haskell, due to purity and type-safety. However, thinking in terms of state transitions at all may be counterproductive here.

[0atman]

Uh oh, the second result on google for "mizar haskell" is THIS SO QUESTION!!1 :-(

[Fred Foo]

This was a quick run through Google and CiteseerX. This Mizar paper was published in an academic journal, though not a high-profile one.

[C. A. McCann]

@Oatman: Really, the main benefit of Haskell for this purpose is how much you can do without even needing external tools. Just avoid IO, general recursion, and partial functions wherever possible (which for most programs is "nearly everywhere, with a bit of effort").

[C. A. McCann]

@Oatman: That doesn't mean much. Stack Overflow has crazy-go-nuts google juice. Questions about niche topics can easily beat out primary sources.

[0atman]

Quite right guys, but information on mizar is very thin on the ground, not the pre-existing package that I was hoping for. I'll add it to my reading list!

[0atman]

@camccann: I like the domain-specific idea. A dialect of Haskell designed to be provable! Is this something I'm going to have to have a go at, or has work already been done on something similar, to your knowledge?

[mokus]

smallcheck as well - smallcheck is like quickcheck, but focuses on exhaustively testing "small" cases, for a configurable notion of "small".

[C. A. McCann]

@Oatman: Geez, Haskell programmers love program correctness. You can find little fragments of that sort of thing all over the place; e.g., the whole point of the IO monad is to provide guaranteed ordering of side effects despite lazy evaluation without letting pure code observe any impurity. But for a more in-depth example, take a look at ImProve on Hackage.

[C. A. McCann]

I recall also seeing a package somewhere that would automatically produce quickcheck tests based on algebraic properties, such as stating a distributive law for two functions would produce checks that f x (g y z) always equals g (f x y) (f x z).

[sclv]

To be a possibly wrong pedant, you probably mean "no efficient method" since one could just exhaustively enumerate and test successively longer proofs, probably subject to some sort of increasing amount of "fuel" to avoid Halting gotchas :-)

[C. A. McCann]

@sclv: And here's a method for solving the Halting problem: Just run the program indefinitely and wait to see if it ever halts. How do you know when to stop enumerating proofs? In short, you can look for proofs that way, but you can't distinguish "no proof exists" from "no proof found (yet)".

[Heinrich Apfelmus]

I chose an appropriate definition of "method" that already includes the efficiency concerns. ;-)

[Tom Crockett]

Coq does indeed have an "extract to Haskell" feature

[0atman]

Thanks, I'll check it out, though I'm really looking for a pure-language way of model checking. Translation from a more formal language to Haskell is sub-optimal for general use.

[svenningsson]

No, it's the other way around. Haskell is translated to Isabelle. It might still not be optimal but it's probably better for your purposes than the Coq approach of generating Haskell.

[0atman]

Oh oh oooh! Sorry I mis-read your answer. Hmm, that's unusual and more useful!

[David Thornley]

Arithmetic can be a problem. Theoretically, if you know the size of all results, including the intermediate ones, you can make guarantees. Practically, many computations do not lend themselves to this. Without arbitrary-sized integers, proving arithmetic correct is tricky. For floating-point, consider docs.sun.com/source/806-3568/ncg_goldberg.html (What Every Computer Scientist Should Know About Floating Point), and that this is after a lot of very bright people tried to make floating point tractable.

[dan_waterworth]

Any idea when ESC/Haskell will be available in ghc?

[sclv]

@dan_waterworth -- I don't know of any plans in that direction, unfortunately.

[dan_waterworth]

shame, I could really do with it for a project I'm working on. Thanks for replying.

[Robin Green]

Check out also Lazy Smallcheck, which leverages Haskell's lazy evaluation.

[recursion.ninja]

Also, Haskell's SmallCheck library will exhaustively check a property for a range of values on an Enum. Very practical for "one-off" (not recomputing for each build) proofs of some Enum's properties.