[xgk]

   Depending on the programming 
   language being proved

That's true, GCed languages are simpler in this regard. But for low-level languages you have to do this 'by hand', and it can be complicated.

   not had the concept of null

That doesn't make the problem go away, you just have another case in the destructors (e.g. pattern matching) that you need to account for logically. Just kicking the can down the road.

   would love to read more 
   about it

Nothing published. Long story. I'll tell you in person, should we meet some day.