[plt-scheme] type of language

On Dec 9, 2009, at 4:17 PM, hendrik at topoi.pooq.com wrote:
>> 
>> A statically-typed language is one with a built-in proof system that 
>> demonstrates the impossibility of certain runtime errors.  These 
>> languages refuse to run any programs for which their proof system 
>> cannot construct such a proof.
> 
> A statically typed language is one in which the types of expressions 
> and variables and such can be determined without running the program.  
> It only manages to be a proof in the sense you describe if the type 
> system is strong as well.

I wouldn't call such a language statically typed.  

I would agree with you, though, that (in addition to my earlier definition) a type system must associate "types" (whatever those are) with "terms" (whatever those are).

Ultimately, of course, definitions such as this are decided in the court of popular opinion.  My arguments in this court are observed not to have much effect.

John


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2484 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20091209/1386c28f/attachment.p7s>