A new kind of programming language

The intuitionistic programming language (IPL) is a new open source programming language, implemented in OCaml, combining a very high level of abstraction with compilation to efficient LLVM bytecode.

The semantics of IPL is intuitionistic type theory without recursive types. Type-theoretic constructs, such as lambda abstraction, pairing, and proof objects, are eliminated at compile time using a new algorithm which translates any type-theoretic term of base type, in a context where all variables are of base type, into clean LLVM bytecode.

See http://intuitionistic.org for more information.

Mathematics and computer science

Mathematics, logic, and computer science share a common history. Mathematics and logic are ancient dragons, and not much upheaval is to be expected in their futures. But where lies the future of computer science?

Many philosophers of the 20th century embraced a view going back, at least, to Leibniz, viz., that, by using a formal language where all assumptions are made explicit, most differences in opinion can be solved by tracing the differences back to different (implicit) assumptions. It becomes evident, by reading a newspaper, e.g., that this view, though of great potential, has not had a large impact in the domains of every-day life.

Computer science would seem to be much more fertile soil for such ideas, and this makes it all the more surprising that computer programming is an activity performed by people who, by and large, have little or no knowledge about formal languages and formal methods.^[1] Since at least three decades, the computer industry is full of buzzwords with little or no real signification. How many products, packages, and technologies have not promised to empower their users beyond what is reasonable to expect?

There seems to be no evidence that the quality of newly written software is better than the quality of old software. In many application domains it even seems to be worse. This is partially explained by the increasing complexity of software and the thin spread of competent programmers: a disastrous combination. Appeals for more scientific and rigorous approaches to IT-projects have been voices crying in the desert.^[2] This unfortunate development is a consequence of the human mind meeting the unrelenting computers, without sufficient respect for the complexity of the problem at hand. The obvious but tedious solution is the application of logic.

There are two approaches to logic in computer science. The first approach is to apply some logical formalism, e.g., propositional logic, to a conventional programming language. The second approach is to replace the conventional programming language with a language designed by logicians. In the former case we speak about formal methods and in the second case we speak about formal languages. The language advocated here, Martin-Löf’s type theory, is of the second kind, i.e., a formal language: type theory is not an add-on to a conventional programming language, but a programming language in its own right.^[3]

Though Martin-Löf’s type theory usually is associated with functional programming, there is no real reason to limit its application to batch computing. Haskell’s monad system, and the many interactive programs written using it, shows that the style of programming dubbed functional also can handle interactive programs.^[4] The long term goal of much ongoing research on Martin-Löf’s type theory is to enable programmers to write complete applications using the language of Martin-Löf’s type theory, including graphical user interfaces, web interfaces, business logic, workflows, integration components (e.g, Web Services, COM+, CORBA, etc.), system calls (Win32, POSIX, etc.), database interaction (e.g., ODBC), native code interoperability, and database schemata.

There is no royal road to software correctness. Martin-Löf’s type theory is a great tool, but we also need a method to address the quality problems of software: “Controlling complexity is the essence of computer programming”. Therefore, we, programming language designers, software architects, and computer programmers, have to face the hard facts and deal with the problems accordingly. At this point I think it is fitting to review Descartes’ method of rightly conducting the reason. In his Discours de la méthode he writes that he thought that the following four precepts are sufficient:^[5]

• “The first was never to accept anything for true which I did not plainly know to be such; that is to say, carefully to avoid hasty judgement and prejudice, and to include nothing more in my judgements than what presented itself to my mind so clearly and so distinctly that I had no occasion to call it in doubt.
• The second, to divide each of the difficulties I would examine into as many parts as possible and as was required in order better to resolve them.
• The third, to conduct my thoughts in an orderly fashion, by commencing with those objects that are simplest and easiest to know, in order to ascend little by little, as by degrees, to the knowledge of the most composite things, and by supposing an order even among those things that do not naturally precede one another.
• And the last, everywhere to make enumerations so complete and reviews so general that I was assured of having omitted nothing.”

I think that these four points, conceived in 1637, form a much more realistic and rigorous ground for software correctness than, most modern project methodologies.

Descartes’ four precepts codify a mathematician’s way of approaching a problem. To my mind, there is no essential difference in how a computer programmer ought to approach a practical programming problem. Indeed, Martin-Löf’s type theory is both a foundation for constructive mathematics and for computer programming.

“In fact, I do not think that the search for high level programming languages that are more and more satisfactory from a logical point of view can stop short of anything but a language in which (constructive) mathematics can be adequately expressed”^[6]

The appeal for a programming language of mathematical rigor is even more urgent today, when we develop larger and larger systems. If the confidence in software is to be maintained, the links with mathematics and logic that computer science had in its infancy must be maintained and nurtured. By its very nature, Martin-Löf’s type theory is a very important link between the three subjects.

References

^[1] Cf., E. W. Dijkstra “On the role of scientific thought”, pp. 60-66, In Selected Writings on Computing: A Personal Perspective, Springer-Verlag, 1982 (PDF).
^[2] Again, cf., E. W. Dijkstra, op. cit.
^[3] Cf., Martin-Löf, “Constructive mathematics and computer programming”, 1982 (PDF).
^[4] I take the existence of the book Real World Haskell to be a constructive proof of this claim.
^[5] Descartes, Discours de la méthode, Ch. 2, transl. D. A. Cress.
^[6] Martin-Löf, op. cit., last sentence.

Software composability

On Channel9, there an interesting interview with Anders Hejlsberg, Herb Sutter, Erik Meijer and Brian Beckman from Microsoft.

http://channel9.msdn.com/shows/Going+Deep/Anders-Hejlsberg-Herb-Sutter-Erik-Meijer-Brian-Beckman-Software-Composability-and-the-Future-of/

One of my mantras is that compositionality is the key to programming language design and software architecture. It is great to hear that some of the greatest minds at Microsoft agree!

Three perspectives on the application

Let us consider the the notion of application from three different perspectives: from the user’s perspective, from the architect’s perspective, and from the perspective of Martin-Löf’s type theory. 

Assuming an interactive application, the first thing that strikes the user is, of course, the graphical user interface and its aestetic aspects, such as colour and shape. After that we have the ergonomic aspects, usability aspects, or interaction design, such as logical placement of buttons and menus, proper choice of controls, proper rating and aggregation of information, etc. 

Next we have the dynamic aspects of the application: the commands that the application supports and their proper implementation. For example, when checking out a shopping cart, money must be drawn and gods delivered. 

Finally we have the user’s view of the entities of the application, such as products, and shopping carts for a web-shop. These entities have relations between them, e.g., a shopping cart contains products. Moreover, entities have attributes, e.g., a product has a delivery status. These three, entities, relations, and attributes, can be called static aspects. This summarizes the user’s view of the application. 

We now turn our attention to the architect’s view. Here the ordering of the aspecs is different, indeed, often the reverse: while the user’s view follows the order of knowning (ordo cognoscendi), the architect’s view follows the order of being (ordi essendi), or, better, the order of conceptual priority. Moreover, while the user deals with individuals, the architect deals with universals. 

The architect considers the same static aspects as the user, albeit as universals rather than as particulars, i.e., he considers the entity book instead of this or that particular book. He also considers the same dynamic aspects as the user, but, again, universally instead of individually.  

With proper separation of concerns, the aestetic aspects need not be the concern of the architect. However, the ergonomic aspects are difficult to separate completely from the static and dynamic aspects, as the former depend on the latter. For example, one cannot display attributes that are not in the static model or aggregates that are not computable. Similarly, the dynamic model may limit the ergonomic design: perhaps one cannot pay before choosing delivery address because the shipping cost differs between addresses. 

To my mind, the correct order of conceptual priority is: static, dynamic, ergonomic. Although designing things in this order will not work if the static or dynamic models make unrealistic simplifications of actual problem domain. For example, the architect may allow only one delivery address per invoice while the ergonomic design requires the user to be able to pick delivery address per invoice line: here the static model is in error. The conceptual priority is correct, but reality is prior to every concept. On could say that the ergonomic aspects ought to have a corrective function on the static and dynamic models. 

Having said this much about the user’s and architec’s perspective of an application, it is time to have a look at how all artifacts that the architect deals with can be captured within the framework of Martin-Löf’s type theory. Martin-Löf’s type theory deals with 

• types, and
• objects of types.

Although the perspective of Martin-Löf’s type theory seems very limited compared to the user’s and architect’s perspectives, it in fact encompasses both in the sense that the user’s and architect’s notions can be given logically satisfactory definitions in type theory. In general, the notions of the architect become types and the notions of the user become objects.