What is Expressiveness in a Computer Language

[Chris F Clark]

Chris Smith <cdsmith at twu.net> writes: 
 
> I thought about this in the context of reading Anton's latest post to
> me, but I'm just throwing out an idea. 
 
I think there is some sense of convergence here.  In particular, I 
reason about my program using "unsound types".  That is, I reason 
about my program using types which I can (at least partially) 
formalize, but for which there is no sound axiomatic system.  Now, 
these types are locally sound, i.e. I can prove properties that hold 
for regions of my programs.  However, the complexity of the programs 
prevent me from formally proving the entire program is correct (or 
even entirely type-safe)--I generally work in a staticly, but 
weakly-typed language.  Sometimes, for performance reasons, the rules
need to be bent--and the goal is to bend the rules, but not break 
them.  At other times, I want to strenghten the rules, make parts of 
the program more provably correct.
 
How does this work in practice?  Well, there is a set of ideal types, 
I would like to use in my program.  Those types would prove that my 
program is correct.  However, because there are parts of the program 
that for perfomnace reasons need me to widen the ideal types to 
something less tight, pragmatic types.  The system can validate that I 
have not broken the pragmatic types.  That is not tight enough to 
prove the program correct, but it provides some level of security.
 
To improve my confidence in the program, I borrow the tagging concept 
to supplement the static type system.  At key points in the program I 
can check the type tag to ensure that the data being manipulated 
actual matches the unprovable ideal type system.  If it doesn't, I 
have a witness to the error in my reasoning.  It is not perfect, but 
it is better than nothing.
 
Why am I in this state, because I believe that most interesting
programs are beyond my ability to formally prove them, or at least
prove them in "reasonable" time bounds.  Therefore, I prove
(universally quantify) some properties of my programs, but many other
(and most of the "interesting") properties, I can only existentially
quantify--it worked in the cases that it was tested on.  It is a
corrolary of this, that most programs have bugs--places where the
formal reasoning was incomplete (did not reason down to relevant
interesting property) and the informal reasoning was wrong.

Thus, the two forms of reasoning, static typing to check the formal
properties that it can, and dynamic tagging to catch the errors that
it missed work like a belt and suspenders system.  I would like the
static type system to catch more errors, but I need it to express more
to do so, and many of the properties that are interesting require
n-squared operations to validate.  Equally important, the dynamic tags
help when working in an essentially untrustworthy world.  Not only do
our own programs have bugs, so do the systems we run them on, both
hardware and software.  Moreover, alpha radiation and quantum effects
can change "constants" in a program (some of my work has to do with
soft-error rates on chips where we are trying to guarantee that the
chip will have a reasonable MBTF for certain algorithms).  That's not
to ignore the effects of malware and other ways your program can be
made less reliable.

Yes, I want a well-proven program, but I also want some guarantee that
the program is actually executing the algorithm specified.  That
requires a certain amount of "redundant" run-time checks.  Knuth had a
quote about a program only being proven and not tested that reflects
the appropriate cynicism.

I consider any case where a program gives a function outside of its
domain a "type error", because an ideal (but unacheivable) type system
would have prevented it.  That does not make all errors, type errors,
because if I give a program an input within its domain and it
mis-computes the result, that is not a type error.

-Chris