What is Expressiveness in a Computer Language

[Chris Smith]

Chris F Clark <cfc at shell01.TheWorld.com> wrote:
> These informal systems, which may not prove what they claim to prove
> are my concept of a "type system".

Okay, that works.  I'm not sure where it gets us, though, except for 
gaining you the right to use "type system" in a completely uninteresting 
sense to describe your mental processes.  You still need to be careful, 
since most statements from type theory about type systems tend to 
implicitly assume the property of being sound.

I'm not exactly convinced that it's possible to separate that set of 
reasoning people do about programs into types and not-types, though.  If 
you want to stretch the definition like this, then I'm afraid that you 
end up with the entire realm of human thought counting as a type system.  
I seem to recall that there are epistemologists who would be happy with 
that conclusion (I don't recall who, and I'm not actually interested 
enough to seek them out), but it doesn't lead to a very helpful sort of 
characterization.

> It is to the people who are reasoning informally about
> the program we wish to communicate that there is a type error.  That
> is, we want someone who is dealing with the program informally to
> realize that there is an error, and that this error is somehow related
> to some input not being kept within proper bounds (inside the domain
> set) and that as a result the program will compute an unexpected and
> incorrect result.

I've lost the context for this part of the thread.  We want this for 
what purpose and in what situation?

I don't think we necessarily want this as the goal of a dynamic type 
system, if that's what you mean.  There is always a large (infinite? I 
think so...) list of potential type systems under which the error would 
not have been a type error.  How does the dynamic type system know which 
informally defined, potentially unsound, mental type system to check 
against?  If it doesn't know, then it can't possibly know that something 
is a type error.  If it does know, then the mental type system must be 
formally defined (if nothing else, operationally by the type checker.)

> I also stress the informality, because beyond a certain nearly trivial
> level of complexity, people are not capable of dealing with truly
> formal systems.

I think (hope, anyway) that you overstate the case here.  We can deal 
with formal systems.  We simply make errors.  When those errors are 
found, they are corrected.  Nevertheless, I don't suspect that a large 
part of the established base of theorems of modern mathematics are 
false, simply because they are sometimes rather involved reasoning in a 
complex system.

Specifications are another thing, because they are often developed under 
time pressure and then extremely difficult to change.  I agree that we 
should write better specs, but I think the main challenges are political 
and pragmatic, rather than fundamental to human understanding.

> Therefore, I do not want to exlcude from type systems, things wich are
> informal and unsound.  They are simply artifacts of human creation.

Certainly, though, when it is realized that a type system is unsound, it 
should be fixed as soon as possible.  Otherwise, the type system doesn't 
do much good.  It's also true, I suppose, that as soon as a person 
realizes that their mental thought process of types is unsound, they 
would want to fix it.  The difference, though, is that there is then no 
formal definition to fix.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation