[Prev][Next][Index][Thread]

RE: type safety

> Either Xi and Pfenning only handle trivial cases or their type system
> must set a new record for complexity.  A sophisticated approach to
> eliminating array bounds checks involves solving integer linear
> programming problems.  Are you stating that all type systems
> that do not incorporate integer programming solvers are "very simple"?

Judge for yourself.  It's essentially restricted to linear 
inequalities for which a number of good algorithms apply.  
And, as someone pointed out with lists, using aggregate operators 
(e.g., iterators) reduces the number of individual cases that 
require the programmer to insert an explicit test.  The key
is that (a) the test is explicit and (b) can be moved across
interfaces.  

So yes, I'll go so far as to say that next-generation type
systems should incorporate some integer programming.  

> On a more serious note, what you are proposing is to replace
> conventional static type systems generated by simple syntactic rules
> with much more complex static analyses akin to what Matthias and I
> call "soft type systems".  

There's a long history of this.  Other projects include the
wonderful extended static checking at Compaq SRC, lclint and
its follow-ons at MIT, the work of Henglein, etc.

> What I fail to see is why these analyses (which can be
> very expensive computationally) should be incorporated in the language
> syntax.  

Two reasons.  First, I've found that the soft-typing approach
for Scheme doesn't work well unless you program in a very
stylized fashion -- in particular, you must use Andrew Wright's
wonderful pattern matching system to get decent results.  This
suggests that development of the type system should go hand-in-hand
with the language and that getting good results is as much a
function of getting programmers to meet the type-checker in the
middle as it is for sophisticated analyses.  This is half of
the "user interface" issue I mentioned earlier.

Second, soft-typing, unlike conventional type systems, ESC, lclint, etc.
does not provide a notation for expressing invariants or interfaces.
This is important not only from a methodological point of view,
but also from a practical one, if verification is to be at all
scalable.  In particular, when designing program units, libraries,
classes, etc. we can't have the set of contexts in which it will
be used.  

The design of this notation for expressing invariants is a 
language design that requires a lot of careful thought.  If
it's not designed as a language, then programmers have no 
portable way of expressing their intention or interfacing
to the analysis tools.  In addition, when integrated into
the language (or at least environment), a compiler can take
advantage of the invariants.  And finally, the ability to
explicitly state invariants is crucial for giving understandable
feedback to the programmer when the analysis fails.  In
particular, the programmer needs to understand whether
the failure is due to an incompleteness in the analysis,
an inconsistency in the specification, or indeed, a bug in
the code w.r.t. the specification.  In turn, this implies
that the analysis being performed should be easily internalized
by a programmer, else all they get is a mysterious error
that they'll just hack around until the analysis finally
seems to succeed.  (Indeed, one could argue that ML-style inference
skates on the edge of going too far for programmers to understand
the analysis.)

Having said all this, soft typing is still useful as is any
verification tool.  But specification is, IMHO, just as 
necessary.  I agree that it's not necessary for the specification
language to be integrated with the base language, especially
since this allows us to experiment with more aggressive
kinds of invariants and analyses.  ESC is a perfect example.
But I expect that the advantages of smooth integration with
the underlying language will mean that we eventually evolve
to incorporate the useful analyses into the base language.

-Greg