On Thursday 12 February 2009 14:09:41 Michael G Schwern wrote: > I hope somebody writes a provable kernel.
Why? It would be practically useless unless they proved all cases of input (user and hardware), in which case it would only be practically useless for every case which lacks complete proofs. See also "Why writing a Fibonacci generator in Haskell demonstrates almost nothing interesting about Haskell." -- c