This started off with points (1) and (2) - code size and abstraction matching. I've said I think they're related, and I've talked about why I think compilers need more abstractions that better match with people, and why people need more abstractions in general (possibly inspired by existing compiler abstractions). Notice about (1) that if the program is truely trivial, then it's decidable, so everything about it can be known statically. You can even think of it as its own type :) As soon as the program becomes undecidable, I claim that understanding the program is equivalent to knowing the program's type in some ideal type system for that problem.
At POPL last week, there was a neat paper that ties together (1) and (2) quite nicely. The Design and Implementation of Typed Scheme. These guys were working with PLT Scheme, which is an untyped lisp dialect designed and used as a scripting language. They found that they could design a type system which would type check the vast majority of real (bug free) programs written in their community. It's quite neat - you can type up a module at a time. As data crosses the module boundary, it's checked dynamically. All the internals are statically checked. If you type check two modules that talk to each other, the dynamic checks between them aren't necessary any more. So, a 100% dynamic program performs the same as a 100% static program (there's no static performance optimisation yet). A hybrid program has a slight slowdown because of the dynamic checks at the boundaries, but it's not a lot.
They were motivated by (1) (they had a problem of maintainability as things scaled up, which they wanted to solve with explicit typing) and they were constrained by (2) (their type abstraction had to match real code written by real dynamic programmers).
In their talk, they mentioned investigating applying these techniques to ruby, python, etc in future work. Pretty exciting stuff.
no subject
At POPL last week, there was a neat paper that ties together (1) and (2) quite nicely. The Design and Implementation of Typed Scheme. These guys were working with PLT Scheme, which is an untyped lisp dialect designed and used as a scripting language. They found that they could design a type system which would type check the vast majority of real (bug free) programs written in their community. It's quite neat - you can type up a module at a time. As data crosses the module boundary, it's checked dynamically. All the internals are statically checked. If you type check two modules that talk to each other, the dynamic checks between them aren't necessary any more. So, a 100% dynamic program performs the same as a 100% static program (there's no static performance optimisation yet). A hybrid program has a slight slowdown because of the dynamic checks at the boundaries, but it's not a lot.
They were motivated by (1) (they had a problem of maintainability as things scaled up, which they wanted to solve with explicit typing) and they were constrained by (2) (their type abstraction had to match real code written by real dynamic programmers).
In their talk, they mentioned investigating applying these techniques to ruby, python, etc in future work. Pretty exciting stuff.