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

RE: type safety


Hi Greg,

In a recent posting, you asserted:

>... 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.  

I don't know where you got this idea but it is false.  Both SoftScheme
and MrSpidey permit the programmer to annotate programs with
invariants.  Support for such a facility is central to the philosophy
of soft typing.  In essence, soft typing is a restricted form of program
verification that relies on static analysis rather than unrestricted
theorem proving to prove that program operations do not fault.

Our soft typers for Scheme do not require programmers to annotate
their code with invariants because we believe that Scheme programmers
would never accept such a prescriptive tool.

For the record, neither lclint nor ESC is a bona fide soft type system
because both systems are unsound.  ESC conceivably could be recast as
a sound inference system if it excluded certain classes of errors.  In
contrast, lclint is purely heurstic.

In general, I fail to see the myriad distinctions that you are making
between soft typing and static typing.  Soft typing clearly depends a
well-chosen language for expressing type assertions just like static
typing.  Moreover, it can and does use exactly the same form of
analyses.  The only essential difference between our approach and
yours is that we decouple complex static analyses from the definition
of what constitutes a well-formed program.

The complex part of the type system can be separated from the language
definition and encapsulated in a separate tool called a soft type
checker.  All of the same compiler optimizations that are applicable
of a rich static type system are applicable in the context of the
corresponding soft type system.  The compiler simply performs much
less optimization if the information extracted by soft type analysis
is not available.

-- Corky Cartwright