Re: cheerful static typing (was: Any and Every... (was: Eval))

[Dan Weinreb <address@hidden>]

   Date: 10 Jan 2002 12:31:00 -0500
   From: jmarshall@mak.com

   gregs@ai.mit.edu (Gregory T. Sullivan) writes:

   > Put another way, all programs, for given a static analysis, fall into
   > one of three camps:
   > 
   >   (1) Statically safe - proven to be free of runtime errors.

   This isn't necessarily the case.  You can have a `statically safe'
   program that `throws an exception' or `invokes the error handler' at
   runtime.

You should not equate "runtime error" with "throws an exception".
Some errors do not throw exceptions, and some throws of exceptions are
not errors.  An error is when a program fails to meet its defined
contract.  If you call integer divide on 2 and 0, and it throws a
zero-divide exception, that's not an error, because integer divide
is obeying its contract.

While I'm at it: "statically safe" doesn't really mean that the
program is proven to be correct.  It just means that that progrm
doesn't have certain specific errors, e.g. (depending on the details
of the language) that a value passed as an argument is not of the
declared type.