Chris's Review

Problem Addressed

---

This paper identifies the core idea underlying many fundamental and apparently distinct results over the last ten years of POPL/PLDI research including high-utility results like proof-carrying code, safe low-level languages (C--, bytecode, TAL), and compartmentalized security. The core idea is that with powerful type systems, the Curry Howard correspondence (types ~ formulas, programs ~ proofs) can be applied to prove semantic properties of programs. The question addresses is how can that construction be provided in a lightweight, expressive way that reframes those results.

Key Contributions

---

Sheard presents Omega, a research programming language with a highly-expressive type system containing:

• pure type systems [programming at multiple levels]
• rank-N polymorphism [universal quantifiers allowed within types],
• generalized algebraic data types [user-level typechecking]
• indexed types [generic / parametric types]
• equality-qualified types [equality constraints on types]

but, curiously, not type classes and constructor classes. Staging enables complex programs written in Omega to recover runtime efficiency.

The abstract concentrates on describing Omega, and simply lists thevarious applications of it. The full paper gives code examples of static scoping, staging and efficiency, proof-carrying code, temporal safety (without model checking), and multi-level security.

Last, he compares his system to similar results in theorem-proving environments Coq and Twelf, demonstrating that Omega allows computational content to be directly executed, unlike the proofs in the othertwo systems. This reinforces the notion that a separate property-proving tool is an unnecessary distraction.

Weaknesses

---

The paper depends on a lot of abstract machinery that is not detailed in the paper. Understanding how a particular piece of the puzzle fits and supports the results requires close reading.

It is unclear how much of the work is automatic. In particular, the type system appears to be undecidable (for example, I can embed Peano arithmetic in it); why is the type checking sound? The best approximation I can get is that anything non-trivial must be proven (decided) by the programmer. This leads to type annotations gone wild: 80% of the proof-carrying code example is type annotations (in the guise of type-level programming).

Questions

---

I find the paper full of deliberately provocative statements:

• "languages of the future will have the following features"
• "languages will be within reach of the majority of programmers"
• "this approach ... [is] of interest to all programmers".

Do we agree with these claims?

One line of discussion for our group is to appraise the value his results to our work: are they toy examples that are uninteresting, impractical or unscalable? Is he expressing the kinds of semantic properties that AOP is invested in?

Another line of discussion for our group is audience: can the average programmer be expected to master this highly-abstract style of programming, and apply it in day-to-day work?

A third line of discussion is tool support: assuming this is valuable, what facets can be supplied automatically? One example might be Conor McBride's epigram, where types direct the development of the program.

Ed's Review

Problems Addressed

---

Omega is designed to fill the gap between highly expressive formal reasoning systems and practical programming languages. Although theorem provers and logical frameworks such as 'Coq' allow the devloper to caputure/prove important semantic properties of his program, the process involves a significant amount of effort and results in meta-logical properties external to the program. They present Omega, which is both a practical programming language and a logic. The developer is able to program against a functional programming language interface with a strengthened type system that includes arbitrary rank polymorphism, equality qualified types, extensible kinds and staging support. With minimal effort, the developer is able to express important semantic properties of his program - ensuring the quality of the code produced.

Key Contributions

---

• Omega was a well designed language, and it was described in a clear and concise manor (with practical examples)
• The authors made a good case for the usefulness of such a lanague. (most interesting to me was 'proof carrying code' - section 6 on the more recent version of the paper).
• The language builds effectively on recent advances in the PL community: rank-N polymorphism, staged computation systems, and indexed types.
• A mechanism which supports extension of Omega's logic to deal with both logical(semantic) and physical(resource usage) properties of the system. The latter is achieved through a staging mechanism, which allows the computation system to deal with notions of compile-time, link-time, run-time and run-time code generation.

Weaknesses

---

• the paper makes many presumptions.. both about programmers' wants/needs and about issues or problems with current programming tools.
• the section 3 'an introduction to Omega' provided high-level and low-level discussion simultaneously, making the example kind of hard to follow.
• Figure 2 was not explained well enough.

Questions

---

1. How have these improvements to the type system affected compile time and run time of a program.
2. What are some situations where this type system fails (sending up either false-positives or false-negatives).
3. How robust are systems written in Omega to regular maintenance. Does the tangling of functional and logical code increase cognitive load on the developer?

Navjot's Review

Problem Addressed

---

Programming languages do not allow users to encode semantic information about a program. Theorem provers and logical frameworks are generally used to reason about such information wherever formal methods are used to validate programming designs. The paper aims to reduce the overall costs of employing such formal methods by incorporating elements of formal reasoning systems in a practical, easy-to-use programming language.

Key Contributions

---

• The paper identifies a need to build a lightweight - yet formal- reasoning mechanism into programming languages.

• The central thesis is that a slightly strengthened type system is sufficient to reason about significant semantic properties.The enhanced type system uses GADTs to represent proofs as concrete objects. These 'proofs' enforce semantic properties expressed in types. Other extensions to the type system include arbitrary rank polymorphism, and extensible 'kinds' of types.

Strengths

---

• The concept of programs whose types enforce semantic properties is attractive.
• The ability to perform dynamic property checking by reflecting types to first class values.
• Soundness of computations is guaranteed implicitly (Although I'm not aware exactly how an equality constrained type system is provably sound.)
• I liked the discussion in Section 3 on 'proofs are data that fit together in precise ways'

Weaknesses

---

• It appears possible to encode hard-to-prove/check properties. Some performance numbers to go with the examples would have made for useful anecdotal evidence in this regard.
• The authors make a number of claims that are difficult to establish or refute. For instance, it is not obvious that the gains always justify the effort involved in wrestling with logic.
• I would have liked to see a short discussion on the limitations of Omega vis-a-vis systems like Coq and Twelf. Is it obvious that Omega can represent and check all-or even most- properties that may be checked using the traditional formal system ?

Questions

---

1. Section 7: "Type Functions in Omega" - What does it mean for type functions to be exhaustive and confluent ?
2. What could a similar system for an imperative PL look like?

-- Main.janvik - 06 Jun 2005