[E-Lang] required type annotations lead to more integration bugs (was: ...)

[Mark S. Miller]

At 02:05 PM Friday 3/2/01, zooko@zooko.com wrote:
> Alan wrote:
>> zooko wrote:
>> > [...] start with whatever they felt was easiest while doing
>> > rapid-prototyping and then start adding type annotations as [...]
>> > strike the right balance between rapid coding and bug detection.
>> 
>> Actually, my experience was the opposite for the first Java version of
>> e-speak.  Those developers who cast everything to Object got their stuff to
>> compile quite quickly, and even got some small bits of code to run.
>> However, the first time they had to interact with someone else's code, they
>> spent days tracking down bugs related to type mismatches.
>
>This is the important difference in practice between type *inferencing*
>with optional type annotations 

Agreed.  E is designed (by type theory amateurs, help!) to make possible 
multiple such external static type checkers.  A given shop may decide only 
to allow code to be committed to its main line source tree if it passes such 
a static checker.  However, the language doesn't enforce these extra rules, 
so even in such a shop a programmer can privately experiment by running code 
that they haven't yet gotten to statically type check.

The Hewitt-Lieberman invention of generational GC, and likewise Ungar's 
generation scavenging, rely on the observation that objects have a high 
infant mortality.  Therefore, it's worth checking often whether a young 
object is dead, whereas its better to invest in storage to store more old 
objects, some of which may be undetected garbage.

Similarly, rapid prototyping relies on the observation that code has a high 
infant mortality.  Or it *should*.  Often we figure out what we want to 
write by writing and running something.  While we're just working out ideas, 
we want to kill as many bad ideas off as quickly as possible.  Only for the 
small amount of code that survives this stage should we invest the time it 
takes to pass various static checkers.


                     But let's not forget THE IMPORTANT PROBLEM


Also, and I can't stress this enough, we desperately need static-type-like 
static checkers, but we don't desperately need static type checkers.  A 
static type checker can only save us from runtime NoSuchMethodExceptions or 
ClassCastExceptions, both of which are thrown, and both of which therefore 
normally lead only to fail-stop misbehaviors.

What we desperately need is static checking technology for security 
properties, so that we might catch the next fatal ErtpMintMaker security bug 
even if Hal is paying attention to something else that day.  We can start by 
asking, as MarcS tried, what static checks could have caught (or helped 
catch) the fatal security hole in the earlier ErtpMintMaker before Steve & I 
posted it?


        Cheers,
        --MarkM