Lambda the Ultimate

See here for some examples/demos from Microsoft.

The papers presented at the International Workshop on Software Factories (held at OOPSLA 2005) are avialable online as well.

The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

Alloy has been mentioned before, but with the recent discussions revolving around IDEs and questions about whether some kinds of checking belong in the language or in the tools surrounding the language, I thought it might be worth revisiting. In fact, it's tempting to suggest that we at LtU adopt a new category for stories: "Lightweight Formal Methods," and that we editors attempt to establish a continuum with respect to stories that fit the category. For example, Pierce makes the observation in TAPL that type systems are a particular kind of lightweight formal method, and that one of their benefits is that they're the only kind that are guaranteed to be used. Alloy falls in the "outside the language proper, but still incremental" category, and somewhere else on the spectrum you have full-blown theorem provers like Twelf, Coq, MetaPRL, et al. Does it make sense to try to unify some of the discussions about the boundary between languages and external tools under this umbrella?

An long and interesting rant by Charles Petzold.

Obviously this is mostly about the IDE side of things (seeing as VS is an IDE).

Some of the features that VS provides are intended to overcome the huge size of the standard libraries, and you might argue this isn't really a language issue. At some level this is indeed a valid argument. However, I think we should pause every once in awhile and wonder whether better programming language abstractions might make modern programming - with GUIs, XML etc. - easier, and eliminate some of the need for huge libraries. In fact, one can argue that LINQ (Cw) is a step in this direction, as regards data access.

It is also worth noting that when IDEs influence the way programming is done, they influence the way languages are used, and thus influence the design space. Programmers demand new language features partly as a response to their experience with the language as it is used in practice.

Finally, the impact on teaching and learning programming shouldn't be overlooked. Students naturally want to produce cool GUI applications and use VS. If this makes it harder to introduce them to different programming techniques and languages (and I think it does), this can be highly problematic.

Here are some choice quotes from Petzold (who also said that the whole history of new programming languages... for Windows has involved the struggle to reduce the windows hello-world program down to something small, sleek, and elegant):

To get IntelliSense to work right, not only must you code in a bottom-up structure, but within each method or property, you must also write you code linearly from beginning to end — just as if you were using that old DOS line editor, EDLIN. You must define all variables before you use them. No more skipping around in your code.

If we select a new project type of Windows Application, for example, and give it a name and location on a local drive, Visual Studio generates sufficient code so that this project is immediately compilable and runable... Somehow, we have been persuaded that this is the proper way to program. I don’t know why. Personally, I find starting a program with an empty source code file to be very enjoyable.

This is the file in which Visual Studio inserts generated code when you design your form. Visual Studio really doesn’t want you messing around with this file, and for good reason. Visual Studio is expecting this generated code to be in a certain format, and if you mess with it, it may not be able to read it back in the next time you open the project.

This bothered me because Visual Basic was treating a program not as a complete coherent document, but as little snippets of code attached to visual objects. That’s not what a program is. That’s not what the compiler sees. How did one then get a sense of the complete program? It baffled me.

If Visual Studio really wanted you to write good code, every time you dragged a control onto your form, an annoying dialog would pop up saying “Type in a meaningful name for this control.” But Visual Studio is not interested in having you write good code. It wants you to write code fast.

Singularity is a research project in Microsoft Research that started with the question: what would a software platform look like if it was designed from scratch with the primary goal of dependability? Singularity is working to answer this question by building on advances in programming languages and tools to develop a new system architecture and operating system (named Singularity), with the aim of producing a more robust and dependable software platform. Singularity demonstrates the practicality of new technologies and architectural decisions, which should lead to the construction of more robust and dependable systems...
Singularity... starts from a premise of language safety and builds a system architecture that supports and enhances the language guarantees.

An interesting overview of what sounds like an intersting project.

The choice of implementation language is also interesting:

Singularity is written in Sing#, which is an extension to the Spec# language developed in Microsoft Research. Spec# itself is an extension to Microsoft’s C# language that provides constructs (pre- and post-conditions and object invariants) for specifying program behavior. Specifications can be statically verified by the Boogie verifier or checked by compiler-inserted run-time tests. Sing# extends this language with support for channels and low-level constructs necessary for system code....integrating a feature into a language allows more aspects of a program to be verified. Singularity’s constructs allow communication to be statically verified.

An interesting aspect is the support for meta-programming, which is implemented in an unusal manner:

Compile-time reflection (CTR) is a partial substitute for the CLR’s full reflection capability. CTR is similar to techniques such as macros, binary code rewriting, aspects, meta-programming, and multi-stage languages. The basic idea is that programs may contain place-holder elements (classes, methods, fields, etc.) that are subsequently expanded by a generator.

Many other intersting design decisions are discussed in the paper (e.g., various DbC facilities), so do check it out.

Linear types for aliased resources. Chris Hawblitzel.

Type systems that track aliasing can verify state-dependent program properties. For example, such systems can verify that a program does not access a resource after deallocating the resource. The simplest way to track aliasing is to use linear types, which on the surface appear to ban the aliasing of linear resources entirely. Since banning aliasing is considered too draconian for many practical programs, researchers have proposed type systems that allow limited forms of aliasing, without losing total control over state-dependent properties. This paper describes how to encode one such system, the capability calculus, using a type system based on plain linear types with no special support for aliasing. Given well-typed capability calculus source programs, the encodings produce well-typed target programs based on linear types. These encodings demonstrate that, contrary to common expectations, linear type systems can express aliasing of linear resources.

The prose is slightly confusing, but the code examples help.

Sections 1 & 2 should be enough for those who only want to understand the problem with aliasing, and get a glimpse of what linear types are.

Modular Checking for Buffer Overflows in the Large. Brian Hackett; Manuvir Das; Daniel Wang; Zhe Yang.

We describe an ongoing project, the deployment of a modular checker to statically find and prevent every buffer overflow in future versions of a Microsoft product. Lightweight annotations specify requirements for safely using each buffer, and functions are checked individually to ensure they obey these requirements and do not overflow. To date over 400,000 annotations have been added to specify buffer usage in the source code for this product, of which over 150,000 were automatically inferred, and over 3,000 potential buffer overflows have been found and fixed.

Good to know someone is doing something about buffer overflows...

Culpepper, Owens, Flatt. Syntactic Abstraction in Component Interfaces. GPCE 2005.

In this paper, we show how to combine a component system and a macro system. A component system separates the definition of a program fragment from the statements that link it, enabling indepen­dent compilation of the fragment. A macro system, in contrast, relies on explicit links among fragments that import macros, since macro ex­pansion must happen at compile time. Our combination places macro definitions inside component signatures, thereby permitting macro ex­pansion at compile time, while still allowing independent compilation and linking for the run-­time part of components.

An amusing podcast about, among other things, the programming model appropriate for SOA, and especially whether is should be synchronous or asynchronous.

You'll feel right at home, since the concepts "abstraction" and "state" raise their head quite early into the discussion...

ContextL is a CLOS extension for Context-oriented Programming. Currently, there is no documentation available, but you can find a small test case in the distribution and an introduction to ContextL's features in a first overview paper.

The paper says:

We present ContextL,a language extension for the Common Lisp Object System that allows for Context-oriented Programming. It provides means to associate partial class and method definitions with layers and to activate such layers in the control flow of a running program. When a layer is activated, the partial definitions become part of the program until this layer is deactivated. This has the effect that the behavior of a program can be modified according to the context of its use without the need to mention such context dependencies in the affected base program. We illustrate these ideas by describing a way to a)provide different UI views on the same object while b)keeping the conceptual simplicity of OOP that objects know themselves how to behave, in this case how to display themselves. These seemingly contradictory goals can be achieved by separating out class definitions into separate layers instead of separating out the display code into different classes.

Sounds kinda like AOP to me. It intriguings, anyway.

Two interesting articles by Jaron Lanier on how protocols influence programming

SUN Interviev

If you look at the way we write software, the metaphor of the telegraph wire sending pulses like Morse code has profoundly influenced everything we do. For instance, a variable passed to a function is a simulation of a wire. If you send a message to an object, that's a simulation of a wire.

WHY GORDIAN SOFTWARE HAS CONVINCED ME TO BELIEVE IN THE REALITY OF CATS AND APPLES

If you model information theory on signals going down a wire, you simplify your task in that you only have one point being measured or modified at a time at each end. It's easier to talk about a single point in some ways, and in particular it's easier to come up with mathematical techniques to perform analytic tricks. At the same time, though, you pay by adding complexity at another level, since the only way to give meaning to a single point value in space is time. You end up with information structures spread out over time, which leads to a particular set of ideas about coding schemes in which the sender and receiver have agreed on a temporal syntactical layer in advance.