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.
