[bitc-dev] Primary type arithmetic

Jonathan S. Shapiro shap at eros-os.org
Tue Feb 8 09:43:00 EST 2005


On Mon, 2005-02-07 at 17:22 +0100, Lorens Kockum wrote:
> One thing that I like with Java is the explicit specification in
> function definitions of all exception types that the function is
> permitted to throw.

In my opinion, this was a very serious mistake. The problem is that it
simply doesn't work, because it doesn't scale across multi-
organizational collaborations.

Developer in organization A writes function a(). This function calls
function b() written by a second developer in organization B. Because
the function b() throws an exception, a() must declare that it too can
throw that exception (or must catch it).

Developer A dies tragically, leaving many orphaned customers in the
field with code that works adequately.

Company B now upgrades their library, and that function b() now is
repaired to fix some bug. The fix requires that b() must now throw some
new exception that it could not previously throw. The exception is low
likelihood. Work is completed, and the upgrade ships.

Users of A's code, who probably never triggered the bug in B's code, now
spontaneously discover that their application no longer runs.

For high-assurance code, exceptions must surely be dealt with, and it is
appropriate to state a theorem that the application doesn't throw any.
It *may* be appropriate to state theorems that a given procedure f()
only throws certain exceptions (which is a good bit stronger than just
declaring them).

> It seems to me that such a definition is quite in line with
> the bitc philosophy. It forces one to think hard about error
> conditions.

While I agree that error conditions are important things to think about,
statements like "it forces one to think hard about error conditions"
have become so hackneyed that they lack any force.

There is a dynamic tension here. Declaring thrown exceptions is, in
effect, declaring a theorem. The tension is that if we encourage people
to use simpler mechanisms, they'll never get pulled into the theorem
definition world.

It isn't immediately clear what to do here.


shap



More information about the bitc-dev mailing list