Comment by wyager
12 years ago
Speaking of proofs, how about we write security critical code in haskell? You need a very simple runtime, but beyond that it would work pretty much wherever.
Most memory-related bugs are automatically eliminated, and security proofs are easier.
If you haven't seen it already, check out Cryptol from Gallois: http://corp.galois.com/cryptol/
It's a crypto DSL that I believe is implemented in Haskell (it compiles to Haskell, C, C++ and a few others).
Particularly relevant example: TLS/SSL implementation in Haskell.
http://hackage.haskell.org/package/tls
Virtually all code exposed to the Internet is security critical, however.