The nullephant in the room is that procedural programming with mutable state (registers, class fields, whatever) is not trivially amenable to logical analysis, and any constraints introduced to rectify this issue become the topic of a never-ending river of tutorials and navel-gazing rants on the demerits of said tutorials. (See borrow-checkers, linear/affine types, monads etc.)
People want to Get Stuff Done, and preferably without getting all math-y about it. Compile now plz.
Add the null-reference to your spec and Presto! the problem is now confined to userspace.
it can be done, but it's Not Fun, and definetly mathy, e.g. Predicate Transformers or ß-reductions