Provable Code

• You can also prove that some code is correct.
• This is important for some critical systems (like life support on the space shuttle), but is also important for a large range of code that you want to make bullet proof.
• The basic idea is that a function has a range of possible inputs. You assert that it gets only those.
• You can also assert that the outputs are correct, but that's harder, so you can assert the outputs are legal. That's less of a proof but still helps.
• This is advocated by Grice in his book the Science of Programming. It works, but of course takes extra work.
• An assertion is a bit of code that crashes or puts up a fault if it is false. For example, in C assert (i > 0); If i == 0 it puts up an error and exits.
• You might, reasonable say that assertions will slow the code down.
• That's what the debug compiler flag is for.
  void assert(bool x) {
  #ifdef debug
  if (!x) error();
  #endif
  }
  
• If you're in debug mode all the stuff is there. If not, it goes away.
• You can do this in other languages too.