What is Expressiveness in a Computer Language

[Dr.Ruud]

Marshall schreef:

Rob Thorpe:

Well, of course you can't in *C*; you can barely zip you pants with C.
But I believe you can do the above in C++, can't you?

You can write self-modifying code in C, so I don't see how you can not
do that in C.

 

[Darren New]

You can write self-modifying code in C,

No, by violating the standards and invoking undefined behavior, you can
write self-modifying code. I wouldn't say you're still "in C" any more, tho.

 

[David Hopwood]

[...]

That text goes back at least 20 years, to R3RS in 1986, and possibly
earlier, so part of what it represents is simply changing use of
terminology, combined with an attempt to put Scheme in context relative
to multiple languages and terminology usages. The fact that we're still
discussing this now, and haven't settled on terminology acceptable to
all sides, illustrates the problem.

The Scheme report doesn't actually say anything about how latent types
relate to static types, in the way that I've recently characterized the
relationship here. However, I thought this was a good place to explain
how I got to where I am on this subject.

There's been a lot of work done on soft type inference in Scheme, and
other kinds of type analysis. The Scheme report talks about latent
types as meaning "types are associated with values". While this might
cause some teeth-grinding amongst type theorists, it's meaningful enough
when you look at simple cases: cases where the type of a term is an
exact match for the type tags of the values that flow through that term.

When you get to more complex cases, though, most type inferencers for
Scheme assign traditional static-style types to terms. If you think
about this in conjunction with the term "latent types", it's an obvious
connection to make that what the inferencer is doing is recovering types
that are latent in the source.

But these types are not part of the Scheme language. If you combine Scheme
with a type inferencer, you get a new language that is not R*RS Scheme,
and *that* language is typed.

Note that different inferencers will give different type assignments.
They may be similar, but they may also be quite dissimilar in some cases.
This casts considerable doubt on the assertion that the inferencer is
"recovering types latent in the source".

 

[Marshall]

Marshall schreef:

You can write self-modifying code in C, so I don't see how you can not
do that in C.

I stand corrected: if one is using C and writing self-modifying
code, then one *can* zip one's pants.


Marshall

 

[Chris Smith]

I thought about this in the context of reading Anton's latest post to
me, but I'm just throwing out an idea. It's certainly too fuzzy in my
mind at the moment to consider it in any way developed. I'm sure it's
just as problematic, if not more so, as any existing accounts of dynamic
types. Here it is, anyway, just because it's a different way of seeing
things.

(I'll first point out here, because it's about to become significant,
that contrary to what's been said several times, static type systems
assign types to expressions rather than variables.)

First of all, it's been pointed out several times that static typing
assumes a static program, and that it becomes difficult to describe if
the program itself is being modified as it is evaluated. The
interesting thing that occurred to me earlier today is that for
languages that are reducible to the lambda calculus at least, ALL
programs are from some perspective self-modifying. Specifically, no
single expression is ever evaluated more than once. When a statement is
evaluated several times, that simply means that there is actually a more
complex statement that, when it is evaluated, writes a new statement,
which consists of a copy of itself, plus something else. Thus it makes
little sense, from that perspective, to worry about the possibility that
an expression might have a different type each time it's evaluated, and
therefore violate static typing. It is never evaluated more than once.

What if I were to describe a dynamically typed system as one in which
expressions have types just as they do in a static type system, but in
which programs are seen as self-modifying? Rather than limiting forms
of recursion for well-typed programs to, say, the standard fixed-point
operator and then assigning some special-purpose rule for it, we simply
admit that the program is being modified as it is run. Type inference
(and therefore checking) would need to be performed incrementally. When
they do, the results of evaluating everything up to this point will have
changed the type environment, providing more information than was
previously known. The type environment for assigning types to an
expression could still be treated statically at the time that the
expression first comes into existence; but it would be different then
from what it was at the beginning of the program.

Of course, this is only a formal description of the meaning, and not a
description of any kind of a reasonable implementation. However, this
initially appears, on the surface, to take us some distance toward
unifying dynamic types and static types.

At least two interesting correlations just sort of "fall out".

First, Marshall has observed (and I agree) that static and dynamic types
form not different ways of looking at verifying correctness, but rather
different forms of programming in the first place. It appears to be
encouraging, then, that this perspective classifies static and dynamic
types based on how we define the program rather than how we define the
type checking.

Second, type theory is sometimes concerned with the distinction between
structural and nominal types and various hybrids. We've concerned
ourself a good bit in this thread with exactly what kinds of "tags" or
other runtime type notations are acceptable for defining a dynamically
typed language. In this view, Smalltalk (or some simplification thereof
wherein doesNotUnderstand is considered an error handling mechanism
rather than a first-class part of the language semantics) would
represent the dynamic version of structural types, whereas type
"tagging" systems with a user-declared finite set of type tags would be
the dynamic equivalent to nominal types. Just like in type theory,
dynamic type systems can also have hybrids between structural and
nominal types.

Obviously, that has a lot of problems... some of the same ones that I've
been complaining about. However, it has some interesting
characteristics as well. If an expression is assumed to be different
each time it is encountered, then type the type of "one" expression is
easy to evaluate in the initial environment in which it occurs (for some
well-defined order of evaluation).

Now, to Anton's response, with admittedly rather liberal skimming
(sorry!) to avoid my staying up all night thinking about this.

It's obviously going to be difficult to formally pin down something that
is fundamentally informal. It's fundamentally informal because if
reasoning about the static properties of terms in DT languages were
formalized, it would essentially be something like a formal type system.

We may be talking past each other, then, but I'm not particularly
interested in the informal aspects of what makes up a type. I agree
that formalizing the notion appears quite difficult, especially if my
conjecture above were to become part of it.

However, there are some pretty concrete things we can look at. One of
them, which as I've mentioned elsewhere is part of what led me to my
position, is to look at what a soft type inferencer does. It takes a
program in a dynamically typed language, and infers a static type scheme
for it (obviously, it also defines an appropriate type system for the
language.) This has been done in both Scheme and Erlang, for example.

How do you account for such a feat in the absence of something like
latent types?

There are undoubtedly any number of typing relations and systems of
rules which can be assigned to any program in a dynamically typed
language. I think the more interesting question is how these type
inference systems choose between the limitless possibilities in a way
that tends to be acceptable. I suspect that they do it by assuming
certain kinds of type systems, and then finding them. I doubt they are
going to find a type system in some language until the basics of that
system have been fed to the software as something to look for.

I'd be delighted to discover that I'm wrong. If nothing else, it would
mean that applying these programs to significant amounts of Scheme and
Erlang software would become an invaluable tool for doing research in
type theory.

I think that's a severe understatement.

Yes, I agree. I did not intend the connotations that ended up there.
In fact, I'd say that something like 90% (and yes, I just grabbed that
number out of thin air) of reasoning performed by programmers about
their programs could be performed by a static type system.

BTW, I notice you didn't answer any of the significant questions which I
posed to Vesa. So let me pose one directly to you: how should I rewrite
the first sentence in the preceding paragraph to avoid appealing to an
admittedly informal notion of type?

I'll try to answer your question. My answer is that I wouldn't try. I
would, instead, merely point out that the notion of type is informal,
and that it is not necessarily even meaningful. The two possibilities
that concern me are that either reasoning with types in this informal
sense is just a word, which gets arbitrarily applied to some things but
not others such that distinctions are made that have no real value, and
that any sufficient definition of type-based reasoning is going to be
broad enough to cover most reasoning that programmers ever do, once we
start applying enough rigor to try to distinguish between what counts as
a type and what doesn't. The fact that programmers think about types is
not disputed; my concern is that the types we think about may not
meaningfully exist.

Note, also, that I'm using the word
in the sense of static properties, not in the sense of tagged values.

In the static sense of types, as I just wrote to Chris Uppal, I can then
definitively assert at least the second of the two possibilities above.
Every possible property of program execution is a type once the problem
of how to statically check it has been solved.

For now, I'll stand on what I've written above. When I see if or how
that doesn't convince you, I can go further.

To be clear, I am certainly convinced that people talk and think about
types and also about other things regarding their programs which they do
not call types. I am concerned only with how accurate it is to make
that distinction, on something other than psychological grounds. If we
are addressing different problems, then so be it. If however, you
believe there is a type/non-type distinction that can be built on some
logical foundation, then I'd love to hash it out.

I agree that in the narrow context of considering to what extent a
dynamically typed language has a formal static type system, you can call
it untyped.
OK.

However, what that essentially says is that formal type
theory doesn't have the tools to deal with that language, and you can't
go much further than that. As long as that's what you mean by untyped,
I'm OK with it.

I can see that in a sense... yes, if a specific program has certain
properties, then it may be possible to extend the proof-generator (i.e.,
the type checker) to be able to prove those properties. However, I
remain inconvinced that the same is true of the LANGUAGE. Comments in
this thread indicate to me that even if I could write a type-checker
that checks correctness in a general-purpose programming language, and
that language was Scheme, there would be Scheme programmers who would
prefer not to use my Scheme+Types language because it would pester them
until they got everything perfect before they could run their code, and
Scheme would remain a separate dynamically typed (i.e., from a type
theory perspective, untyped) language despite my having achieved all of
the wildest dreams of the field of type theory. In that sense, I don't
consider this a limitation of type theory.

(Two notes: first, I don't actually believe that this is possible, since
the descriptions people would give for "correct" are nowhere near so
formal as the type theory that would try to check them; and second, I am
not so sure that I'd want to use this new language either, for anything
except applications in which bugs are truly life-threatening.)

Think of it like this: the more ambitious a language's type system is,
the fewer uncaptured static properties remain in the code of programs in
that language. However, there are plenty of languages with rather weak
static type systems. In those cases, code has more static properties
that aren't captured by the type system.

Yes, I agree with this.

I'm pointing out that in many
of these cases, those properties resemble types, to the point that it
can make sense to think of them and reason about them as such, applying
the same sort of reasoning that an automated type inferencer applies.

It often makes sense to apply the same sort of reasoning as would be
involved in static type inference. I also agree that there are
properties called types, which are frequently the same properties caught
by commonly occurring type systems, and which enough developers already
think of under the word "type" to make it worth trying to change that
EXCEPT when there is an explicit discussion going on that touches on
type theory. In that latter case, though, we need to be very careful
about defining some group of things as not-types across the scope of all
possible type systems. There are no such things a priori, and even when
you take into account the common requirement that a type system is
tractable, the set of things that are not-type because it's provably
impossible to check them in polynomial time is smaller than the
intuitive sense of that word.

Essentially, this use of "type" becomes problematic when it is used to
draw conclusions about the scope, nature, purpose, etc. of static types.

This answers a good number of the following concerns.

A complete formal definition of what I'm talking about may be impossible
in principle, because if you could completely formally define it, you'd
have a static type system.

That may not actually be the case. Lots of things may be formally
defined that would nevertheless be different from a static type system.
For example, if someone did provide a rigorous definition of some
category of type errors that could be recognized by some defined process
as such, then the set of language features that detect and react to
these errors could be defined as a type system. Chris Uppal just posted
such a thing in a different part of this thread, and I'm unsure at this
point whether it works or not. The problem with earlier attempts to
define type errors in this thread is that they either tend to include
all possible errors, or are distinguished by some nebulously defined
condition such as being commonly thought of in some way by some set of
human beings.

If that makes you throw up your hands, then all you're saying is that
you're unwilling to deal with a very real phenomenon that has obvious
connections to type theory, examples of which I've given above. That's
your choice, but at the same time, you have to give up exclusive claim
to any variation of the word "type".

I really think it's been a while since I claimed any such thing... and
even at the beginning, I only meant to challenge that use of type in
comparing static and dynamic type systems.

I am not so sure, though, about these obvious connections to type
theory. Those connections may be, for example, some combination of the
following rather uninteresting phenomena:

1. Type theory got the word "type" from somewhere a century ago, and the
word has continued to be used in its original sense as well, and it just
happens that despite the divergence of these uses, there remains some
common ground between the two different meanings.

or, 2. Many programmers approach type theory from the perspective of
having some intuitive definition of a type in mind, and they tend to mix
it in with a few of the ideas of type theory in their minds, and then go
off and use the word in other contexts.

Terms are used in a context, and it's perfectly reasonable to call
something a "latent type" or even a "dynamic type" in a certain context
and point out connections between those terms and their cousins (or if
you insist, their completely unrelated namesakes) static types.

Yes, I agree. I'm yet to be convinced that they are completely
unrelated namesakes. I am actually trying to reconstruct such a thing.
The problem is that, knowing how "type" is used in the static sense, I
am forced to reject attempts that share only basic superficial
similarities and yet miss the main point.

The definition of static type system is not in question. However,
realistically, as I pointed out above, you have to acknowledge that type
systems exist in, and are inextricably connected to, a larger, less
formal context.

No, but it certainly seems that the reason behind calling them a "type
system" is being placed very much in doubt. Simply saying static type
system is horribly wrong, and I do it only to avoid inventing words
wholesale... but I greatly regret the implication that it means "a type
system, which happens to be static."

In some senses, this is akin to describing a boat as "a floating
platform". That may be somewhat accurate as a rough definition for
someone who is familiar with platforms but not with boats. It's a
terrible failure, though, in that it implies that being a platform is
the important bit; where actually the important bit is that it floats!
In fact, it may turn out that boats have very little to do with common
platforms... for example, while some boats (barges) have many of the
same properties that platforms do, there are whole other classes of
boats, which are considerably more powerful than barges, that end up
looking very little like a platform at all. If you press hard enough, I
can be forced to admit that there is some kind of connection between
platforms and floating platforms, because after all one has to stand on
something while using a boat, right?

Well, the important part of the phrase "static type" isn't "type" but
"static." Without even having to undertake the dead-end task of
deciding who's got the right to the word "type", let's assume that I
should really be saying some other word, like boat. However, that word
doesn't really exist, so I am stuck with "static type". I just have to
be very careful about explaining that what I mean by type is completely
different from what others mean by type. There is some overlap, which
potentially arises from one of the uninteresting sources I've listed
above, or maybe... just maybe... arises from some actual similarity that
we haven't identified yet. But we still haven't identified it.

This is very much the situation I see ourselves in. I very much want to
agree with everyone's right to use the word "type", but then people keep
saying things that seem to me to be clear misunderstandings that the
important part is the "static", not the "type". When qualification is
not needed

Fundamentally, the important aspect of types, in the static sense, is
that they are used in a formal, syntactic, tractable method for proving
the absence of program behaviors. Even if it turns out that, in
practice, all type systems contain mechanisms for solving a certain
rigorously definable class of problems, that will not be part of the
definition of types, when the word is used in the static sense. So we
can search for a more formal similarity, or we can agree that it's
incidentally true that they sometimes solve the same problems but also
agree that it's pointless and misleading to ever talk about a "type
system" without clarifying the usage either explicitly or by context.
It remains incorrect to relax the degree of formality and talk about
static types in an intuitive and undefinable way, because than they lose
the entire property of being types at all. At that point, it's best to
drop "static", which is not true anyway, and switch over to the other
set of terminology where it makes sense to call them types.

There's a sense in which one can say that yes, the informal types I'm
referring to have an interesting degree of overlap with static types;
and also that static types do, loosely speaking, have the "purpose" of
formalizing the informal properties I'm talking about.

Static types have the property of proving ANY properties of a program
that may be proven. Certainly, research is pragmatically restricted to
specific problems that are (1) useful and (2) solvable. Aside from
that, I can't imagine any competent language designer building a type
system, but rejecting some useful and solvable feature for the sole
reason that he or she doesn't think of it as solving a type error.

But I hardly see why such an informal characterization should bother
you. It doesn't affect the definition of static type.

I hope I've explained how it does affect the definition of a static
type.

This is based on the assumption that all we're talking about is
"well-defined semantics".

Indeed. My statement there will not apply if we find some formal
definition of a dynamic type system that doesn't reduce to well-defined
semantics once you remove the intuitive bits from it.

 

[Chris Smith]

I stand corrected: if one is using C and writing self-modifying
code, then one *can* zip one's pants.

I believe you'd need quite the creative USB-based or similar peripheral
device, as well.

 

[David Hopwood]

I very much agree with the observation that every programmer performs
"latent typing" in his head [...]
But I also think that "latently typed language" is not a meaningful
characterisation. And for the very same reason! Since any programming
activity involves latent typing - naturally, even in assembler! - it
cannot be attributed to any language in particular, and is hence
useless to distinguish between them. (Even untyped lambda calculus
would not be a counter-example. If you really were to program in it,
you certainly would think along lines like "this function takes two
chuch numerals and produces a third one".)

Vesa raised a similar objection in his post 'Saying "latently typed
language" is making a category mistake'. I've made some relevant
responses to that post.

I agree that there's a valid point in the sense that latent types are
not a property of the semantics of the languages they're associated with.

But to take your example, I've had the pleasure of programming a little
in untyped lambda calculus. I can tell you that not having tags is
quite problematic. You certainly do perform latent typing in your head,
but without tags, the language doesn't provide any built-in support for
it. You're on your own.

I can accept that dynamic tagging provides some support for latent typing
performed "in the programmer's head". But that still does not mean that
dynamic tagging is the same thing as latent typing, or that languages
that use dynamic tagging are "latently typed". This simply is not a
property of the language (as you've already conceded).

 

[David Hopwood]

Consider a langauge something like BCPL or a fancy assembler, but with
not quite a 1:1 mapping with machine langauge.

It differs in one key regard: it has a variable declaration command.
This command allows the programmer to allocate a block of memory to a
variable. If the programmer attempts to index a variable outside the
block of memory allocated to it an error will occur. Similarly if the
programmer attempts to copy a larger block into a smaller block an
error would occur.

Such a language would be truly untyped and "safe", that is safe
according to many peoples use of the word including, I think, yours.

But it differs from latently typed languages like python, perl or lisp.
In such a language there is no information about the type the variable
stores. The programmer cannot write code to test it, and so can't
write functions that issue errors if given arguments of the wrong type.

So the hypothetical language, unlike Python, Perl and Lisp, is not
dynamically *tagged*.

 

[David Hopwood]

Marshall schreef:

You can write self-modifying code in C, so I don't see how you can not
do that in C.

Strictly speaking, you can't write self-modifying code in Standard C.

 

[David Hopwood]

I find it too weak, as if to say: "well, ok, it can't actually corrupt memory
as such, but the program logic is still apt go all over the shop"...

Well, it might ;-)

(In case anyone thinks I am being pejorative toward not-statically-typed
languages here, I would say that the program logic can *also* "go all over
the shop" in a statically typed, memory safe language. To avoid this, you
need at least a language that is "secure" in the sense used in capability
systems, which is a stronger property than memory safety.)

 

[David Hopwood]

I'm suggesting that if a language classifies and tags values in a way
that supports the programmer in static reasoning about the behavior of
terms, that calling it "untyped" does not capture the entire picture,
even if it's technically accurate in a restricted sense (i.e. in the
sense that terms don't have static types that are known within the
language).

Let me come at this from another direction: what do you call the
classifications into number, string, vector etc. that a language like
Scheme does? And when someone writes a program which includes the
following lines, how would you characterize the contents of the comment:

; third : integer -> integer
(define (third n) (quotient n 3))

I would call it an informal type annotation. But the very fact that
it has to be expressed as a comment, and is not checked, means that
the *language* is not typed (even though Scheme is dynamically tagged,
and even though dynamic tagging provides *partial* support for a
programming style that uses this kind of informal annotation).

 

[Anton van Straaten]

I can accept that dynamic tagging provides some support for latent typing
performed "in the programmer's head". But that still does not mean that
dynamic tagging is the same thing as latent typing

No, I'm not saying it is, although I am saying that the former supports
the latter.

or that languages
that use dynamic tagging are "latently typed". This simply is not a
property of the language (as you've already conceded).

Right. I see at least two issues here: one is that as a matter of
shorthand, compressing "language which supports latent typing" to
"latently-typed language" ought to be fine, as long as the term's
meaning is understood.

But beyond that, there's an issue here about the definition of "the
language". When programming in a latently-typed language, a lot of
action goes on outside the language - reasoning about static properties
of programs that are not captured by the semantics of the language.

This means that there's a sense in which the language that the
programmer programs in is not the same language that has a formal
semantic definition. As I mentioned in another post, programmers are
essentially mentally programming in a richer language - a language which
has informal (static) types - but the code they write down elides this
type information, or else puts it in comments.

We have to accept, then, that the formal semantic definitions of
dynamically-checked languages are incomplete in some important ways.
Referring to those semantic definitions as "the language", as though
that's all there is to the language in a broader sense, is misleading.

In this context, the term "latently-typed language" refers to the
language that a programmer experiences, not to the subset of that
language which is all that we're typically able to formally define.

Anton

 

[Anton van Straaten]

That's essentially equivalent to giving up. I doubt many people would
be happy with the conclusion that dynamically typed languages are typed,
but have only one type which is appropriate for all possible operations.

I'm not sure if this is what you're getting at, but what you've written
is precisely the position that type theorists take. Having "only one
type which is appropriate for all possible operations" is exactly what
the term "untyped" implies.

That type system would not be implemented, since it's trivial and
behaves identically to the lack of a type system, and then we're back
where we started.

This is why I've suggested that "untyped" can be a misleading term, when
applied to dynamically-typed languages.

Anton

 

[David Hopwood]

Vesa Karvonen wrote:
...


To make the halting problem decidable one would have to do one of two
things: Depend on memory size limits, or have a language that really is
less expressive, at a very deep level, than any of the languages
mentioned in the newsgroups header for this message.

I don't think Vesa was talking about trying to solve the halting problem.

A type system that required termination would indeed significantly restrict
language expressiveness -- mainly because many interactive processes are
*intended* not to terminate.

A type system that required an annotation on all subprograms that do not
provably terminate, OTOH, would not impact expressiveness at all, and would
be very useful. Such a type system could work by treating some dependent
type parameters as variants which must strictly decrease in a recursive
call or loop. For example, consider a recursive quicksort implementation.
The type of the 'sort' routine would take an array of length
(dependent type parameter) n. Since it only performs recursive calls to
itself with parameter strictly less than n, it is not difficult to prove
automatically that the quicksort terminates. The programmer would probably
just have to give hints in some cases as to which parameters are to be
treated as variants; the rest can be inferred.

 

[Anton van Straaten]

Anton van Straaten wrote: ....


But these types are not part of the Scheme language. If you combine Scheme
with a type inferencer, you get a new language that is not R*RS Scheme,
and *that* language is typed.

Sure. So one obvious question, as I've just observed in another reply
to you, is which language programmers actually program in. I'd say that
they certainly don't program in the completely untyped language as
defined by RnRS.

Note that different inferencers will give different type assignments.
They may be similar, but they may also be quite dissimilar in some cases.
This casts considerable doubt on the assertion that the inferencer is
"recovering types latent in the source".

I mentioned this earlier, in a reply to Marshall where I gave an
informal definition of latent typing, which read in part: "Terms in the
program may be considered as having static types, and it is possible to
infer those types, but it isn't necessarily easy to do so automatically,
and there are usually many possible static type schemes that can be
assigned to a given program."

As far as the term "recovering" goes, that perhaps shouldn't be taken
too literally. It's clearly not the case that a latently-typed program
has a single formalizable type scheme which was put there deliberately
by the programmer. But programmers do reason about things like the
types of functions and expressions, and the goal of soft type
inferencers is to find an approximation to what the programmer intended.

Anton

 

[Marshall]

But beyond that, there's an issue here about the definition of "the
language". When programming in a latently-typed language, a lot of
action goes on outside the language - reasoning about static properties
of programs that are not captured by the semantics of the language.

This means that there's a sense in which the language that the
programmer programs in is not the same language that has a formal
semantic definition. As I mentioned in another post, programmers are
essentially mentally programming in a richer language - a language which
has informal (static) types - but the code they write down elides this
type information, or else puts it in comments.

We have to accept, then, that the formal semantic definitions of
dynamically-checked languages are incomplete in some important ways.
Referring to those semantic definitions as "the language", as though
that's all there is to the language in a broader sense, is misleading.

In this context, the term "latently-typed language" refers to the
language that a programmer experiences, not to the subset of that
language which is all that we're typically able to formally define.

That is starting to get a bit too mystical for my tastes.


Marshall

 

[Marshall]

A type system that required an annotation on all subprograms that do not
provably terminate, OTOH, would not impact expressiveness at all, and would
be very useful.

Interesting. I have always imagined doing this by allowing an
annotation on all subprograms that *do* provably terminate. If
you go the other way, you have to annotate every function that
uses general recursion (or iteration if you swing that way) and that
seems like it might be burdensome. Further, it imposes the
annotation requirement even where the programer might not
care about it, which the reverse does not do.


Marshall

 

[Marshall]

| David Hopwood wrote:
| >
| > A type system that required an annotation on all subprograms that do not
| > provably terminate, OTOH, would not impact expressiveness at all, and would
| > be very useful.
|
| Interesting. I have always imagined doing this by allowing an
| annotation on all subprograms that *do* provably terminate. If
| you go the other way, you have to annotate every function that
| uses general recursion (or iteration if you swing that way) and that
| seems like it might be burdensome. Further, it imposes the
| annotation requirement even where the programer might not
| care about it, which the reverse does not do.

simple things should stay simple. Recursions that provably terminate
are among the simplest ones. Annotations in those cases could be
allowed, but not required. Otherwise the system might become very
irritating to program with.

Yes, exactly my point.


Marshall

 

[Chris F Clark]

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

 

[Pascal Costanza]

That is starting to get a bit too mystical for my tastes.

To paraphrase Abelson & Sussman: Programs must be written for people to
read, and only incidentally for compilers to check their types.




Pascal