What is Expressiveness in a Computer Language

[Chris Uppal]

Andreas Rossberg wrote:

[me:]
> > It's worth noting, too, that (in some sense) the type of an object can
> > change over time[*].
>
> No. Since a type expresses invariants, this is precisely what may *not*
> happen. If certain properties of an object may change then the type of
> the object has to reflect that possibility. Otherwise you cannot
> legitimately call it a type.

Well, it seems to me that you are /assuming/ a notion of what kinds of logic
can be called type (theories), and I don't share your assumptions.  No offence
intended.

Actually I would go a little further than that.  Granted that whatever logic
one wants to apply in order to prove <whatever> about a program execution is
abstract -- and so timeless -- that does not (to my mind) imply that it must be
/static/.  However, even if we grant that additional restriction, that doesn't
imply that the analysis itself must not be cognisant of time.  I see no reason,
even in practise, why a static analysis should not be able to see that the set
of acceptable operations (for some definition of acceptable) for some
object/value/variable can be different at different times in the execution.  If
the analysis is rich enough to check that the temporal constraints are [not]
satisfied, then I don't see why you should want to use another word than "type"
to describe the results of its analysis.

    -- chris