Lambda the Ultimate

The ongoing thread On the (Alleged) Value of Proof for Assurance has sparked a discussion about applying the Curry Howard Isomorphism to more than intuitionistic logic and the simply typed LC. All these attempts are rather hand-wavey to me, but the discussion revolves around Isabelle and Coq, neither of which do I know.

Neelk has made it pretty clear that CH does not apply to Isabelle, but it has gotten me wondering.

* Is there a rigorous way to apply CH to a more powerful type system than the simply typed LC?

* Is it nonsensical to try and apply it?

* Does the ability to type-check non-terminating expressions have an impact? Similarly, do existential types? (I'm thinking F-Omega)

* Are there any articles/books that do apply it to more powerful type systems which are accessible to someone without a PhD?

This discussion relates to the recent Advantages of Purity discussion.

My questions can be summarised as: How are effect systems mainly used in current implementations? Are they widely used for source-level(-ish) optimisations? If yes, where? If not, why?

One of the issues raised in the Purity thread was that pure computations are easier to reason about. Effect systems has been proposed to assist reasoning about stateful computations, most prominently by Benton et. al.'s Monads, Effects and Transformations.

However, Benton only proves a limited number of identities (variants of the ones their Exceptions paper (figures 8-10). But I was interested in more equations. Thinking that effect analysis is common in compiler optimisations, I started looking for implementations of effect systems that make use of the analysis to optimise the program.

As Benton's language is a fragment of MLj's intermediate language, that seemed like a good place to start. However, it has been a while since MLj saw some activity, and besides, I couldn't find any reference to compiler optimisations based on effect analysis in MLj.

I then consulted with several colleagues about using effect type systems for optimisations. To summarise that conversation and the look around I had after it:

• Pure code has benefited greatly from optimisations via source-code transformations. e.g., Haskell, especially a la Santos's thesis: Compilation by Transformation in Non-Strict Functional Languages.
• Even in languages that apply source-code transformation optimisations, optimising effectful code is done at the object-code level, and not as source-code optimisations.

What I am wondering is why effectful transformations are not used in practice? Is it because there is missing theory about effectful transformations? Or is it simply because source-code transformations are not nearly as efficient as object-code transformations? If so, what kind of evidence backs this claim up?

The following will be of interest to many of us:

We are sorry to announce that Robin Milner died on Saturday 20th March, in Cambridge, just three days after the funeral of his wife, Lucy.

He will be greatly missed by his family and friends, as well as the academic community.

We are expecting there to be a symposium in due course to provide an opportunity for Robin's many academic colleagues to celebrate him and his work.

From Chloë and Barney Milner

The project is apparently a little on the inactive side, but the code is available, and web searches do still turn up some info: eocl, wikipedia, et. al.

Rosette is a high performance interpreter for the Actor model which has been enhanced with object-oriented mechanisms for inheritance and reflection. With Rosette, the object-oriented programming model and the Actor concurrent execution model are combined to simplify the development of autonomous, distributed agents.

Thomas Lord's recent insistence that a simpler Scheme is possible (including that advanced features such as first-class macros and environments should be provided, with the caveat that their use may be less performant than non first-class devices) has got me to investigate first-class environments.

Way back there's been a bit of discussion of this topic here.

The usual arguments against first-class environments are:

• They're "dangerous". (IMO, dangerous is good. ;))
• They mess up ahead-of-time compilation. (Well, many projects use JITs these days.)

On the pro side, we have:

• They make the language definition significantly simpler. For example, Christian Queinnec's Sharing Code through First-class Environments can provide a clean account of the interactive top-level, as well as a simplified definition of letrec. In Scheme, the top-level is considered hopeless.
• They can describe stuff like module systems and objects (Lee and Friedman: Quasi-Static Scoping: Sharing Variable Bindings across Multiple Lexical Scopes)
• They provide more visibility into the running program, so they make debugging etc easier.
• They're cool and fun. ;)

So my question is: given that JITs are commonplace these days, should first-class environments be reconsidered for inclusion into programming languages?

BitC is back:

As I get ready to leave Microsoft, I'm once again thinking about BitC. I
want to get the implementation and the language definition to a point of
usability, and this seems like a good time to examine some of the things
that I think, in hindsight, were mistakes or might warrant re-examination.
Most of these issues are mundane practical things. A few of them are deeper
design choices/issues.

I didn't really look at BitC till the project went dormant. Now I have, I think it's great. Every language should have a BitC-like implementation layer.

I recently came across the concept of regular expression types, such as in XDuce. The idea seems promising, but the current implementations all seem excessively restrictive (disallowing nontrivial patterns), so I was wondering about the feasibility of further development in this area. The bottleneck for regular types would definitely be in trying to determine subsumption of these types in an automated manner, but I can't seem to find much literature on the subject.

Computationally how hard is it to determine equivalence/subsumption of regular languages in general. Finite? Hard? Easy?

For at least some languages (a+ <: a*) this sort of comparison seems plausible. If this comparison isn't plausible in general, is there any way to foresee which languages are easy to compare/hard to compare?

Ehud is about to be annoyed with me. :-)

I am lately suffering from doubts about whether the value of proof is justfied by its cost. Some questions, in no particular order:

• Proof seems to be an all-in or all-out exercise. There does not seem to be a viable strategy for initial, limited adoption followed by progressive improvement. Type systems seem to be more "continuous" in their adoption options. Given the (admittedly incomprehensible) expressive power of something like ATS, what is the real semantic gap between provers and type systems these days? Do type-based property embeddings offer the possibility of more incremental and more cost/benefit-aware adoption of checking techniques?
• The goal of proof isn't to be correct. It is to be confident. This has two parts: (1) confidence that you got something right, and (2) ability to convince a second party that your confidence is justified. Assume that you succeed in your proof. To what degree has use of a prover inherently failed objective [2]? If the final objective is credible correctness, then there is presumably a trade-off between accuracy and comprehensibility. Does proof (in its current form, at least) err too much on the side of accuracy?
• Given the likelihood of (possibly retrospective) failures of total abstraction, to what degree is confidence in proof misplaced? If so, is the cost of discharge justified?

There is no question in my mind that proof processes generate more robust code. Yet the general concensus seems to be that this robustness is much more an emergent consequence of rigorously understanding the problem then a result of the proof discharge. In this view, the primary benefit of proof (in the context of assurance) is largely to keep the specification "honest". If this is in fact the goal, is proof the best way to accomplish that goal? How much of that goal can be undertaken by type systems?

In a private conversation, Gernot Heiser (NICTA, OK Labs) was recently asked how use of proof impacted their QA costs. As I recall it, his answer was that they run between 1.5x and 2x the end-to-end cost of conventional development and testing, but they achieve much higher confidence. My questions:

• Might there be a better trade-point between cost and value (in the form of confidence)?
• To what degree is their confidence well-founded?

In a second private conversation, Eric Rudder observed that one of the costs of proof-based methodology was a loss of ability to rapidly adapt software to new requirements and new demands. It follows that proof is not always appropriate, and that a more continuous cost/time/benefit option space would be desirable.

My own observation is that in the end, systems need to be robust, and they include components that lie well outside our ability to prove them. In many cases, type can be usefully exploited when proof cannot, and there is a training cost to educating people in both domains.

So finally my question:

Once we step away from formal semantics and PL insights (which are certainly good things), what is the proper role of proof in real-world production? And what is the proper role of advanced type systems?

Hi LtU,

I'm working on the design of a programming language (as I'm sure many of you are). And sometimes I feel the need to brainstorm about a new idea. LtU looks exactly like the kind of community I want to reach. My experience with different programming languages is limited (I'm basically a C++ guy) and I want to learn.

The LtU forum is not meant for design discussions, but I've been allowed to post a link to another discussion group. If you would like to respond, please do it there, not here. Any thoughts would be most appreciated!

Type system design choices

The program for this year's Code Generation conference is now available at: http://www.codegeneration.net/cg2010/programme.php

The conference, now in its fourth year, is Europe's leading event on Model-Driven Software Development.

Highlights include:

- keynotes from (Pragmatic) Dave Thomas and Eelco Visser (Delft University of Technology)

- Language Extension with MPS: Markus Völter (independent/itemis AG) / Konstantin Solomatov (JetBrains, s.r.o.)

- Proven best practices for successful MDD adoption: Steven Kelly & Juha-Pekka Tolvanen (MetaCase)

An early-bird booking period runs until 1st April with up to 20% off booking fees. Full-time academics can also claim a further 20% discount.

The event takes place 16-18 June 2010 in Cambridge, UK.

Visit http://www.codegeneration.net/cg2010/ for more information.