4 ms·

I wonder what makes C so different from Ada where static verifies are used successfully. Is it because typical C code uses way too many pointers making full sta

• pjmlp 9y ago
  Language semantics, most of C errors that lead to memory corruption are simply forbidden in Ada. There is no way to corrupt memory in Ada unless you explicitly import one of the Unchecked packages and ask the compiler permission to do naughty stuff.
• jcelerier 9y ago
  > Ada where static verifies are used successfully. and yet even ADA's standard library sometimes has bugs: http://blog.adacore.com/formal-verification-of-legacy-code http://blog.adacore.com/formal-verification-of-legacy-code
  • pjmlp 9y ago
    Sure, every programming language can have bugs. However C gets the usual set of logical errors, common to any safe programming language, memory corruption caused by lack of checks on memory access and implicit type conversions, and 200+ cases of UB when taking advantage of full compiler optimizations. Reducing the amount of possible errors per line of code is already a plus, even if doesn't remove all of them.
  • touisteur 9y ago
    Note the article you're citing is going from Ada (already strong safety checks, but you can still write bugs, just not a whole class of them) to Spark2014, so formal proof of absence of runtime errors (first) and automated verification of functional properties. Even nicer, in a stdlib, so not a toy example and something to build on... You're showing (thanks !) how to go (with some effort, but not so much) from 'so much safer than C already' to 'no bug let's move on and maybe remove all the runtime checks to get C-like performance or better'. I'd say it looks pretty cool.