Spec#, nullables and more

[Walter Bright]

bearophile wrote:
> 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 just have a hard time seeing that Spec# is an advanced language incorporating 
the latest in comp sci thought when it adds checked exceptions.


> 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.

I think you misunderstand why checked exceptions are such a bad idea. It's not 
just that they are inconvenient and annoying. They decrease security by *hiding* 
bugs. That is the opposite of what you'd want in a high security language.

http://www.mindview.net/Etc/Discussions/CheckedExceptions


Spec# and Cyclone both fall into the trap of making the right thing to do hard, 
and the wrong thing easy.