Spec#, nullables and more

[bearophile]

Walter Bright:

> Checked exceptions are one of those ideas that look great on paper but are an 
> utter failure in practice. As Bruce Eckel pointed out, they are *worse* than 
> useless and *cause* bugs to be inserted into the code.

(Just to avoid possible misunderstandings: I have never suggested to add checked exceptions to D).

I agree that checked exceptions are a pain in a general purpose language. But Spec# isn't a general purpose language, it's designed to be a high integrity language, where the user is supposed to endure some pain in the hope to produce statically verified (and less buggy) programs. So while checked exceptions are probably a bad idea for a handy general purpose language, the authors of Spec# have thought that for the special purposes of Spec# those exceptions are justified. I don't know if they are right (maybe they are wrong, surely not everything in Spec# design is perfect, despite it generally looks like a really well though out language). But you need to keep in account the quite special purpose of Spec# before judging if adding checked exceptions to Spec# is a bad idea.

Bye,
bearophile