Lambda the Ultimate

It seems to me that PL theory focuses on type systems with respect to what they prove about all well-typed programs. It seems to me that PL theory does not focus on type systems with respect to what they can be made to prove about some well-typed programs.

Is my perception of this focus correct, and, if so, is this a good state of affairs?

I am open to the idea that the answer is "yes, that is PL theory's focus, and that is a good state of affairs since the rest is pragmatics, i.e. software engineering, not PL theory." But I guess I wouldn't have asked the question if I didn't have suspicions to the contrary.

Another way of asking it is, does PL theory treat type systems primarily as a way language designers help programmers, and only secondarily as a way language designers help programmers help themselves? Or does it treat neither role as primary? Or are these roles inseparable?

Comments?

I haven't found anything more on this yet via Googling around; anybody know more? If it really means that all I/O is referentially transparent, it would be interesting to this newbie to see compare/contrast with e.g. Monadic approaches to I/O.

From FOLDOC

It has a continuation-based I/O system with referential transparency and is capable of handling all common I/O tasks such as terminal and file I/O, signal handling and interprocess communications.

Last few years i have been playing with creating my own programming languages, I've got a pretty good idea of what i want it to do and what i want it to look like. I've finally decided to go with the CLR virtual machine as the back end (simply because I'm working on a RAD language and not anything low level. If i need raw speed i will use asm, c, or forth) My problem is that all the common language runtime work i have done has been writing il code for basically toy languages and scripting tools, so while i know what i am getting into as to the ins and outs of compiler design what i don't know is if i could create erlang like green threads in any reasonable manor on the clr.
Anyone have a basic run down of how green threads are implemented in erlang and if i could do something similar on .net?

keep in mind the language will be pure functional sort of like haskell. I have a strong interest in making it erlang like with the concurrency because erlang simply got it right (though the syntax sucks).

Even if all you have is a link i'm cool with that, i'm not afraid to do a lot of research on my own =P