4 ms·
Elephant in the room of having provable algorithms is in real numbers representation limitations in any imaginable hardware (hello irrational numbers!). You sim
by bitL 10y ago
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.
- nickpsecurity 10y agoHuh? 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.
- bitL 10y agoI 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.
- nickpsecurity 10y agoI'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?