Elephant in the room of having provable algorithms is in real numbers representation limitations in any imaginable hardware (hello irrational numbers!). You simply can't make complete proofs for most math-intense problems. Combinatorics should be fine though.
Huh? I might have missed your point but I'm talking about how C makes no effort toward correctness of results. The rest that do to varying degrees sacrifice some performance to get that. Can't speak on the proofs as it's not my specialty. Far as real numbers, that's what analog computers do with some models for making it more general purpose.
I was just going one step further due to my experience in proving correctness of algorithms in functional languages. You probably had on mind usual array safety checks and control flow stuff for which aspects were invented, I raised the bar a bit by pointing out that there are some fundamental issues which even super functional purists can't overcome, so the overall talk about code safety is kinda funny ;-) You will still crash Space Shuttle if you are running on Haskell, just in a different fashion than with C.
I've rarely seen what you're describing although I know plenty work remains go be done. So, could you give examples of code injections or mission-ending errors at code level that Haskell toolchains or Isabelle/HOL couldnt handle?
