[plt-scheme] Re: plt-scheme type of language

On Dec 13, 2009, at 1:29 PM, hendrik at topoi.pooq.com wrote:

> It wsa with Algol 68 that I encountered what I learned to call a strong 
> type system, to contrast with a weak type system.  A strong type system 
> actually had the rigidity to implicitly prove that values would at run 
> time, always be of the types they were declared with.  It baffles me 
> that languages without this property have remained in the mainstream as 
> long as they have.


This idea has become known as "sound" type system, because 
one can explain types a proof system 

  assumptions about types |- expression : type

and one can then show that this kind of proof is sound with
respect to a model -- the run-time execution in this case -- 
just like when you study logic. 

So one can now say that C/C++ have a type system but it is 
unsound. It doesn't predict what happens at run-time. (They 
also have one that is sound but the normal programmer doesn't
even perceive this system.) 

-- Matthias