Lambda the Ultimate

I see the cryptographic community making proofs on code they write. I see static analysis used to validate certain properties of "simplified" C in "real" embeded systems but how much business is really done that uses formal methods to support their development.

Now the reason I mention this, and this is not new, that there has always been a chasm between the "academic" understanding of using mathematically oriented ideas to do things with software and the real life of hiring a developer to get a project done.
I was wondering if this community felt that things were improving.

My personal experience is not good but I will admit that looking at others I am feeling a bit more up-beat these days. Any one want to share their thoughts?

The Lisp family has macros that allow you to generate new code by manipulating programs; S-expressions are used as the representation. For many uses, this is what makes it hard to work with. Manipulating program language in such a low-level form is difficult. Looking at Stratego/XT, the authors clearly indicate that performing program manipulation with ATERMS (Stratego's underlying, low-level term representation, analogous to s expression data) is quite difficult and undesirable. Stratego has mechanisms to deal with program manipulation in a more natural way.

My read of Stratego shows that they authors allow the direct use of program fragments in the language being manipulated as a short form for underlying aterms.

What this boils down to is this: What is the best representation of a program to use, when the program must be manipulated/transformed? Are different representations appropriate for runtime manipulation (a program manipulating itself) vs. build-time manipulation?

Lisp chooses S-Expressions. Java programs can be transformed at compilation or runtime by bytecode manipulation -- aspect-oriented programming can be used to solve problems similar to those macros are generally applied to. C++ performs build-time transformation via its template mechanisms. Scala provides flexible, extensible syntax that relies on efficient compilation to deliver transformation-like behavior. Boo (a .NET language) provides, as a part of its standard library/compiler the ability to modify the AST of the program; there is no inconvenient "detour" through syntax.

This leads me to these thoughts:

1. To the extent is can, the type system of a language should provide as much transformational power (templates/type parameters) as it can. The transformational power of a type system, it seems to me, is just as important as type-safety/correctness.
2. Syntax extensions can result in highly readable code, and as such provide oft-needed flexibility. A good test here is building syntax for array-language operators; does the code "look" as natural as that for atomic values? Does it perform well?
3. Programs increasingly operate in an environment of fluid metadata, and must be able to adapt. Therefore, transformation at runtime is highly desirable.
4. Completeness dictates that transformations should be able to construct other transformations. This necessitates runtime transformations.
5. Losing the transformative and corrective powers of type systems seems undesirable when constructing transformations in general -- are type-safe transformations at runtime any different from those performed by compilers?

Modern VMs perform just-in-time compilation; selective optimized compilation of programs is performed. When new code is dynamically generated, that code is folded into the same JIT framework as "normal" code. When existing code is modified, a VM will "de-optimize", then allow further optimization to occur when needed. If a program's type system is modified, is it possible to perform similar work? In general, it seems that a comprehensive model for the evolution of a program's full AST+Data (types/logic/data) is needed. Lisp does this without checks and balances. Is a given transformation of a program acceptable?

Perhaps there is a kind of bitemporal typed lambda system out there somewhere; something that understands what the type system used to be, what we think it is now, and allows both to be combined together in computation. :)

I'm a freshman in college and... after a lot of thought, I want to do programming language research for a living, or at least something that involves a lot of PLT (perhaps compilers and interpreters for embedded platforms, etc.)... currently I'm working on a double major in Electrical & Computer Engineering and Computer Science. I've really started to wonder lately if I need the engineering aspect of it, or if I should change to something like Computer Science and Mathematics. Which would be better preparation for a career in PLT research?