Is there any large formally verified project written in Haskell? The most well known ones are C (seL4 microkernel) and Coq+OCaml (CompCert verified C compiler).
Well, Haskell has GADTs, new type wrappers and type interfaces which can be (and are often) used to implement formal verification using meta programming, so I get the point he was making.
You pretty much don’t need to plug another language into Haskell to be satisfied about certain conditions if the types are designed correctly.
Those can all encode only very simplistic semantics of the code. You need either a model checker or dependent types to actually verify any kind of interesting semantics (such as "this sort function returns the number in a sorted order", or "this monad obeys the monad laws"). GADTs, newtypes and type interfaces are not significantly more powerful than what you'd get in, say, a Java program in terms of encoding semantics into your types.
Now, I believe GHC also has support for dependent types, but the question stands: are there any major Haskell projects that actually use all of these features to formally verify their semantics? Is any part of the Haskell standard library formally verified, for example?
And yes, I do understand that type checking is a kind of formal verification, so in some sense even a C program is "formally verified", since the compiler ensures that you can't assign a float to an int. But I'm specifically asking about formal verification of higher level semantics - sorting, monad laws, proving some tree is balanced, etc.
seL4 has a Haskell implementation. It only runs under a simulator (as opposed to on real hardware). Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version.
I admit that I was not aware of their use of Haskell, so thanks for bringing this up! It motivated me to go and actually read (parts of) their paper [0].
> Their main proof strategy is to prove the Haskell version correct; then prove the C version matches the Haskell version.
However, I don't think this is right. By my understanding of the paper, the Haskell implementation isn't proven to be correct, it's more of a prototyping tool. The Haskell version is used as an intermediate representation that can be automatically translated into Isabelle/HOL and quickly proven to have various properties. If the proofs don't work at this level, it's easy to change, re-translate, and re-check. To make it easily tramslatable to Isabelle/HOL, they forego many Haskell features, such as typeclasses, or making use of laziness. The Haskell program is also designed to match the eventual C implementation, so it's using C-like data types, pointers, etc - not native Haskell data structures,nor making use of the Haskell GC.
The proofs achieved at this level apply to the auto-generated Isabelle/HOL translation of the Haskell code. The Haskell runtime is not modeled here in any way, and as such the proofs do not hold for the Haskell executable code that you can run on the simulator.
The Haskell prototype was then translated manually to C, trying to keep as close to a 1:1 translation as possible, while still allowing various micro-optimizations. Then, the exact C code was manually translated back to Isabelle/HOL, where they also had a complete model of the semantics of every C statement that they used (they use a subset of C, with the biggest missing feature being references to local variables - you can't use &x if x is a local variable in their C code). Isabelle/HOL was then used to check that this manually written implementation implemented the abstract specification with all of the proven guarantees.
So, the Haskell part was ultimately a convenience, not a fully necessary part of the proof (though the whole thing would probably not have been feasible had they not used it). It was a decent middle ground between being possible for the kernel devs to define the code in it, and the formal verification guys to translate it to Isabelle and verify it. If they had tried to write the C code directly, the cost of translating any change to the C code back to Isabelle for verification would have been too high. Conversely, having the kernel devs learn enough Isabelle to define the prototype code directly in Isabelle would have also been too complicated as well - and I believe the Isabelle code could not be easily executed to be able to do more regular debugging on it during the development process, the way the Haskell code could be run on the simulator.
Is there any large formally verified project written in Haskell? The most well known ones are C (seL4 microkernel) and Coq+OCaml (CompCert verified C compiler).