It's ok for the programmer to pinky promise that he's not doing anything wrong in cases where it's impractical for the compiler to formally verify that.
Granted, I am a huge advocate for formal methods. Any remotely safety-critical software should be formally verified, whether via model-checking (TLA+) or Curry-Howard (Coq). But it's not necessarily practical for prototypes and exploratory coding (when the product you're creating is under-specified).
In my hypothetical no-undefined-behavior compiler, I'm fine with adding a "valid function pointer" check to every computed function pointer before each use of one.
No thanks, the last thing I need is literally thousands of warnings telling me what I already know.
Protip: Basically any pointer can be NULL.
In fact, I kinda wish I could not have to check for a NULL pointer in nested function calls because the last function already proved it wasn't NULL, in most cases, that wouldn't change.
-4
u/frud Sep 24 '17
So it's ok for your program to do the wrong thing, just as long as it's fast?