Ok, I can see the interlocking state machines introducing complexity that is unavoidable but the rest of it just seems like self-inflicted nonsense. I'm more th

Ok, I can see the interlocking state machines introducing complexity that is unavoidable but the rest of it just seems like self-inflicted nonsense. I'm more than willing to take a performance hit and have a correct implementation that is easy to reason about in some high level language than one that every other week is shown to be broken because of some dangling pointer in some patch committed 2 years ago. I don't think I'm the only one with this opinion. I'm sure many others would take the performance hit just so they could have the piece of mind that the underlying crytopgraphic library securing their application's data is actually formally verified. The best part about the high level implementation is that it will only get better over time because of improvements in compiler technology. I'm not much of a conspiracy theorist but this one seems too well placed to be an accident and as long as people can't reason about the mess that is openssl stuff like this is gonna continue to slip in. We have formally verified browser kernels but yet we can't have something as fundamental as SSL/TLS be formally verified. The formally verified browser kernel: http://goto.ucsd.edu/quark/ http://goto.ucsd.edu/quark/. Edit: My google foo is very weak these days. Trending story is https://github.com/vincenthz/hs-tls https://github.com/vincenthz/hs-tls, an implementation of SSL/TLS in Haskell.