Combinators for contracts

The work of Peyton Jones and Eber on specifying financial contracts with combinators (How to write a financial contract) has often cropped up here, but hasn't, I think, ever had its own story.

Since Yale has a vistor, Christian Stefenson, presenting a talk on Enterprise Resource Planning ( A Declarative Framework for Enterprise Systems), which based on the work of Peyton Jones & Eber, I thought it might be timely to raise this very interesting idea.

Some links

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

must...learn....haskell....

I work in the financial industry and I have been trying to get through the financial contracts paper. I wish there was either a haskell class offered in the NYC area or a video similar to the famous SICP videos.

By the way, if some is interested in offering a haskell class, outside of several universities in the New York region, the best venue is probably "New York Institute Of Finance." They are a for-profit organization that offers courses for people in the financial industry. The lecturers get paid...don't know how much. (I am not affiliated with NYIF, but know of its positive reputation).

Haskell classes (a plug)

We do offer a FP course on our part-time professional MSc in Software Engineering at Oxford. Unlike most classes, it is a one-week intensive course, and our students come from all round the world; I usually have at least one student from North America and have had several from the finance industry. You'd be very welcome!

great

Thanks, I didn't know about this!

Haskell video lectures online

Slides and papers online

I have made the materials from today's talk available online.

Also see my main page:
Christian Stefansen

"Smart Contracts"

Nick Szabo's work on "Smart Contracts", in which any protocol (or object-oriented program) can be seen as a contract, seems to be relevant here. If the underlying language provides capability security then the object-oriented program or protocol actually enforces the contract in a strict sense. The real issue is that the language provides security (both in the language's semantics and the language's implementation, the latter requires cryptography); not whether it is functional or object-oriented or whatever. Almost any modern language provides enough abstraction ability to represent what is needed. But it's clear that manipulating combinators in a garden-variety object-oriented language is a little bit more cumbersome than in a language such as Haskell that has proper support for higher-order programming!

From the Lambda Wayback Machine :-)

Peter's right, of course, and we've talked about Smart Contracts a bit before (going back to 2003, in at least one instance): here and my somewhat intemperate, but hopefully useful, comment here; search the page for "smart contract" to get to the specific comment.

For what it's worth, I think Tim Sweeney is right on the money with respect to where he thinks the next mainstream programming language needs to go, but I was disappointed to see that his talk didn't mention security at all. In addition to reliability and concurrency, I would argue that the next mainstream language needs to get security profoundly right, which to me looks like taking the lessons from the object-capability security community and implementing them in a typed setting, drawing from Flow Caml and "An extension of HM(X) with bounded existential and universal data-types", mentioned here, for a type system that combines the dynamic bits with the static bits.

Next mainstream language

In addition to reliability and concurrency, I would argue that the next mainstream language needs to get security profoundly right

I agree with this; this is one of the things I am going to touch on in my FLOPS 2006 invited talk. But I don't think that the next mainstream language will get it right. Maybe the one after that will, ten years from now. If you're in Japan this April, please drop by!

Ten years for security?

Why do you think it will take two generations of languages and ten years? Is it because the right approach is not known, or just a lack of emphasis?

Adoption Rate

I can't presume to speak for Peter, but I can think of reasons Peter might be right: first, I make the assumption that we want security in a typed setting. There's original work to be done there even if you take Flow Caml as a launching-off point.

But before we even get there, a connection needs to be made between the object-capability security community's efforts and any typed setting, as the best extant example of an object-capability programming language—E—is dynamically typed. My intution tells me that the lessons of E can be mapped to the type system of Flow Caml plus the work hinted at in "An Extension of HM(X) with Bounded Existential and Universal Data-Types," but that needs proving.

Finally, there are the obvious issues of probably doing something insufficient the first time, and the cycle of adopting yet another language that gets it right the second time. Such factors alone can easily introduce a decade into the widespread-adoption schedule.

Ten years for security

For security you need message passing as the default and support for the principle of least authority (POLA). Current languages have shared state as the default and current operating systems have poor support for POLA: they have access control lists as the default. Those two wrong defaults will take time to correct! I just hope that in the meantime we will not give up our fundamental freedoms because of the mistaken idea that computers need centralized rights management and enforcement. With POLA and message passing, virus problems go away with almost no effort. This is well-known in the E community and looked at with unbelief by the mainstream. I highly recommend the talk The SkyNet Virus: Why it is Unstoppable; How to Stop it.

Another datapoint

Ed Felten links to a paper that backs up your point

Report: Many Apps Misconfigure Security Settings

From Ed synopsis...

Which brings us to Sudhakar and Andrew’s research. They built an automated tool to analyze the access control settings on files, registry entries, and other objects on a Windows machine. The tool looks at the settings on the machine and applies a set of inference rules that encode the various ways a user could try to leverage his privileges improperly.

...

Sudhakar and Andrew ran the tool on professionally-managed Windows systems, and the results were sobering. Several popular applications, from companies like Adobe, AOL, Macromedia, and Microsoft, had misconfigured their access control in ways that allowed relatively unprivileged users — in some cases even the lowliest Guest account — to gain full control of the system.

Document assembly

An FT story from Wednesday, Lawyers witnesseth dreadful legalese. Following a discussion of a very expensive lawsuit that turned on a crucial ambiguity involving rival interpretations that differed only on placement of a comma, the main point is made:

According to Ken Adams, ... almost any standard business agreement will be riddled with punctuation ambiguities, meaningless boilerplate language and botched verb usage.

The article does search for solutions to this problem in the direction of machine-checkable semantics, but rather document assembly systems, which are less ambitious than the approaches in the story, in that they do not generally attempt to model how the contract will be perfomed, or fail to be performed, but rather attempt to ensure the absence of unintended ambiguity.

The key text seems to be: T. F. Gordon (1992). A theory construction approach to legal document assembly. From pp.211-25 Expert Systems in Law, ed. A. A. Martino.