What is Expressiveness in a Computer Language

[Joe Marshall]

Chris Smith wrote:
> Joachim Durchholz <jo at durchholz.org> wrote:
> > Assume a language that
> > a) defines that a program is "type-correct" iff HM inference establishes
> > that there are no type errors
> > b) compiles a type-incorrect program anyway, with an establishes
> > rigorous semantics for such programs (e.g. by throwing exceptions as
> > appropriate).
>
> So the compiler now attempts to prove theorems about the program, but
> once it has done so it uses the results merely to optimize its runtime
> behavior and then throws the results away.  I'd call that not a
> statically typed language, then.

You're assuming that type-correctness is an all-or-nothing property
(well, technically it *is*, but bear with me).  What if the compiler is
unable to prove a theorem about the entire program, but *can* prove a
theorem about a subset of the program.  The theorems would naturally be
conditional, e.g.  `Provided the input is an integer, the program is
type-safe', or time-bounded, e.g. `Until the program attempts to invoke
function FOO, the program is type-safe.'

Of course, we could encode that by restricting the type of the input
and everything would be copacetic, but suppose there is a requirement
that floating point numbers are valid input.  For some reason, our
program is not type-safe for floats, but as a developer who is working
on the integer math routines, I have no intention of running that code.
 The compiler cannot prove that I won't perversely enter a float, but
it can prove that if I enter an integer everything is type-safe.  I can
therefore run, debug, and use a subset of the program.

That's the important point:  I want to run broken code.  I want to run
as much of the working fragments as I can, and I want a `safety net' to
prevent me from performing undefined operations, but I want the safety
net to catch me at the *last* possible moment.  I'm not playing it safe
and staying where the compiler can prove I'll be ok.  I'm living
dangerously and wandering near the edge where the compiler can't quite
prove that I'll fail.

Once I've done the major amount of exploratory programming, I may very
well want to tighten things up.  I'd like to have the compiler prove
that some mature library is type-safe and that all callers to the
library use it in a type-correct manner.  I'd like the compiler to say
`Hey, did you know that if the user enters a floating point number
instead of his name that your program will crash and burn?', but I
don't want that sort of information until I'm pretty sure about what I
want the program to do in the normal case.