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 co

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.