[mrkeen]

You have it backwards from where I'm standing.

'null' (and to a large extent mutability) drives a gigantic hole through whatever you're trying to prove with correct-by-construction.

You can sometimes annotate against mutability in OO, but even then you're probably not going to get given any persistent collections to work with.

The OO literature itself recommends against using constructors like that, opting for static factory pattern instead.

[munificent]

Nullability doesn't have anything to do with object-oriented programming.

[mrkeen]

Yes, yes, "No true OO language ..." and all that.

But I'm going to keep conflating the two until they release an OO language without nulls.