Void-safety (and related things)

[Joel C. Salomon]

Michiel Helvensteijn wrote:
>>> I doubt it's the direction D wants to go. Because proving correctness at
>>> compile-time requires the holy grail, and testing correctness at runtime
>>> requires extra space for each variable and extra time for each access.
> 
> Basically, if you want to know at compile-time whether a variable is
> initialized, there are several possibilities:
> 
> * Be overly conservative: Make sure every possible computational path has an
> assignment to the variable, otherwise give an error. This would throw out
> the baby with the bathwater. Many valid programs would cause an error.
> 
> * Actually analyze the control flow: Make sure that exactly all reachable
> states have the variable initialized, otherwise give an error. Dubbed "holy
> grail", because this sort of analysis is still some time off, and would
> allow some very cool correctness verification.

Third (stop-gap) option:
• Be conservative, but trust the programmer:  Allow some sort of pragma
to tell the compiler that the programmer has done the flow analysis and
the variable really is set (or non-null, or…).  It will be an unchecked
error to lie to the compiler--until the holy grail is implemented, when
it will become a checked error.

This is a feature of the Plan 9 C compilers (cf. “The compile-time
environment” in <http://plan9.bell-labs.com/sys/doc/comp.html>).

“If you lie to the compiler, it will get its revenge.” —Henry Spencer

—Joel Salomon