[plt-scheme] contracts.ss: Can you disable them at runtime?

On May 17, 2007, at 3:07 PM, Anton van Straaten wrote:

Your metaphors were much much worse than Hoare's; I didn't understand  
a word ;-)

> These risks and costs are going to vary by project, so the  
> designers of a contract system should be careful about second- 
> guessing their users about this.  As the experience with static  
> type systems shows, people will just avoid something entirely if it  
> doesn't give them what they're looking for.  Particularly in this  
> sort of situation, it is better to give users the freedom to do  
> what they think they want, but educate them on how to use it  
> responsibly.

We (I am speaking for Robby and myself) actually agree. But let me  
recount some experience and some principle:

Experience: I worked in industry for around 2 years. The company I  
worked for produced distributed real-time systems for controlling the  
distribution of gas and electricity in small cities. My boss had me  
design and test a piece of software in Pascal and translate it via  
compiler and by hand into 6009 asm. We beat the existing asm system  
by a factor of 2. That's before we took out the array-bound check  
(which can be understood as a contract); after that it was even better.

When we deployed, my boss decided to put the array-bound check back  
in. His insight: all deployed systems are broken. We had some  
customer call in a problem all the time. If the "stuck message" came  
with a reasonable error message, we had a good chance of gracefully  
re-starting the system and even patching in a backpack (an asm  
debugging technqiue) to work around the problem. He found going out  
of array bounds particularly annoying and decided stopping a failing  
system right there and then would be preferable to having the system  
behave in an erratic manner. [Note: I had delivered a Hoare-style  
argument that this couldn't happen. As far as I know, it never did  
happen.]

Principle: I have based the entire contract philosophy for PLT Scheme  
on this insight, which I have encountered time and again. That is:

  1. it is often (but not always) okay to stop a system when an error  
is discovered
  2. all systems contain errors, so 1 is not theory
  3. a good error message, suggesting a place where you should start  
debugging is critical (blame)

Because of this, contracts in PLT have become a generalization of  
safety checks. For decades, people asked for switches to turn them  
off. Indeed, you can turn them off in OCAML -- yes, you read that  
right -- and turn OCAML into unsafe language. Experience suggests,  
however, that this is almost never justified. And it is almost never  
necessary for performance reasons.

Still, we will figure out how to turn off one side of a contract,  
because we know that on rare occasions we need it and we are tired of  
answering this question. We also have a philosophical justification  
due to the nature of our blame-assignment idea.

So wait for the announcement -- Matthias