Just to elaborate a bit more, the use of optional values rather than NULL is really a special case dependent types. It's saying that no type can contain a non-

Just to elaborate a bit more, the use of optional values rather than NULL is really a special case dependent types. It's saying that no type can contain a non-value. For another example, imagine subtracting something from an unsigned int. You need to ensure that the value never goes below zero If you have an expression like 'x - 1', then the compiler needs to ensure that x is always > 0. The nice thing about this kind of static analysis for critical systems is that there are often extreme consequences if a runtime check fails. What do we do for the nuclear power control system when we detect an error? Crash? Shut down the system? But the system is not functioning properly. How do we know that we can safely shut it down? These are pretty horrible things to consider. It's much better to be able to say analytically that the situation can not happen. I once worked in a high energy physics lab, though. There is always memory corruption to contend with, so you'll never be free of runtime errors ;-)