No disagreement, but wanted to point out that groups like Galois have been using Haskell-embedded, compile-to-C DSLs in some interesting ways recently: http://

No disagreement, but wanted to point out that groups like Galois have been using Haskell-embedded, compile-to-C DSLs in some interesting ways recently: http://smaccmpilot.org/images/dronecon-talk.pdf http://smaccmpilot.org/images/dronecon-talk.pdf This has the potential for nice compile-time guarantees without the runtime cost (and potentially at much lower cost than full formal verification) (also, fwiw, Haskell has been around since 1990, making it about 7 years younger than C++)