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

[Guy Steele - Sun Microsystems Labs <address@hidden>]

   Date: Thu, 10 Jan 2002 13:22:04 -0500 (EST)
   From: Dan Weinreb <dlw@exceloncorp.com>
   To: gls@labean.East.Sun.COM
   CC: jmarshall@mak.com, ll1-discuss@ai.mit.edu
   Subject: Re: cheerful static typing (was: Any and Every... (was: Eval))
   
      Date: Thu, 10 Jan 2002 12:59:09 -0500 (EST)
      From: Guy Steele - Sun Microsystems Labs <gls@labean.East.Sun.COM>
   
      Careful, here, Dan; taking this to a logical extreme
      implies that, if you beef up the contracts, you can
      define away all errors.
   
   I really don't understand what you mean by this.
   
   Perhaps you're saying that you could define away all errors by simply
   making the contract be the same as the code.  Well, yes.  But if the
   contract is the same as the code, then who is to say that the code has
   a "bug"?
   
   To put it another way, I don't see what "correct" can mean other than
   that the code does, in fact, provide an implementation of a
   specification of what the code is supposed to do.  If nobody ever lays
   out the answer to the question "what is this code *supposed* to do", I
   don't see how one can objectively say that the implementation is
   correct or not correct.

Couldn't have said it better myself.  In fact, I didn't.
I think we agree most fanatically emphatically.

(If we define my term "undesirable" to mean "that's not what
it's *supposed* to do" in your terms, then I think we said
the same thing.  Part of the confusion arises because I was not
clear about exactly which contract was under discussion.
It's not an error for "/" to throw zero-divide, because that's
in its contract.  It is an error for "prime?" to throw
zero-divide, because that is *not* in its contract.  And
programming errors typically stem from a failure of the
contracts of the individual pieces of a composite language
construct, plus the contract of the composition mechanism(s),
to imply or enforce the desired overall contract.

--Guy