Home » forums » LtU Forum

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

By Charles Stewart at 2006-02-03 15:24 | LtU Forum | previous forum topic | next forum topic | other blogs | 17880 reads

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).

By shahbaz at Fri, 2006-02-03 16:53 | login or register to post comments

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!

By jeremygibbons at Tue, 2006-02-14 11:26 | login or register to post comments

great

Thanks, I didn't know about this!

By shahbaz at Tue, 2006-02-14 15:27 | login or register to post comments

Haskell video lectures online

Haskell video lectures online

By Marsh J. Ray at Sat, 2009-03-28 13:52 | login or register to post comments

More Haskell video lectures

13-part online Haskell course by Erik Meijer at MSDN's Channel9.

By Matt Brubeck at Fri, 2010-04-16 03:57 | login or register to post comments

Slides and papers online

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

Also see my main page:
Christian Stefansen

By cstef at Sat, 2006-02-04 01:16 | login or register to post comments

"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!

By Peter Van Roy at Sun, 2006-02-05 20:08 | login or register to post comments

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.

By Paul Snively at Sun, 2006-02-05 21:07 | login or register to post comments

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!

By Peter Van Roy at Mon, 2006-02-06 14:05 | login or register to post comments

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?

By Jeff Nowakowski at Tue, 2006-02-07 01:05 | login or register to post comments

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.

By Paul Snively at Tue, 2006-02-07 05:47 | login or register to post comments

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.

By Peter Van Roy at Tue, 2006-02-07 11:45 | login or register to post comments

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.

By alnerd at Wed, 2006-02-08 15:40 | login or register to post comments

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.

By Charles Stewart at Fri, 2009-03-27 13:21 | login or register to post comments

30 common patterns

Today's Financial Times published a letter from Willi Brammert, Financial system can be made safer without stifling it, which says:

The variety of financial contracts is much smaller then commonly believed: almost all financial contracts fit into fewer than 30 common patterns. This covers the whole range from saving accounts to exotic options and even alphabet soup contracts such as collateralised debt obligations. Defining those patterns as a standard would create an international financial language.

...

[Were] financial contracts [to be so] commonly understood [this] would even lead to greater safety since the language would cover all contracts, not only structured products. This would penetrate the clouds of mystery that helped nurture the financial crisis by preventing even the chief executives and chairmen of the companies concerned from seeing their own risks (as they pleaded to official bodies).

Brammertz's claim directly supports the importance of the kind of work that Peyton Jones &al. have been doing here. He has a short opinion article on the topic, Standardization of financial contracts, which says a little bit more about the typology of contracts.

By Charles Stewart at Thu, 2010-04-15 20:34 | login or register to post comments

Can't... Resist...

This has nothing to do with anything except for scientists who somehow get infatuated with financial systems.

Has the MONIAC analogue computer ever been mentioned on LtU?

By marco at Thu, 2010-04-15 20:51 | login or register to post comments

Relevance of contract typology

Well, no, I do think this is relevant, and there should be little need to justify these sorts of items. In general, I think that connections between formal methods and law are spot on topic for LtU, and have provoked some research that a good number of people here find interesting. Financial systems are particularly interesting because it seems that financial contracts seem to have a relatively simple, compositional structure, and there has been a lot of effort put into valuing financial contracts, so they have something like a formal semantics.

I'm not about to post these kinds of items to the front page unless there is interesting code or programming language design there, but I'd guess that enough people find these news items interesting to justify posting them.

Am I wrong?

By Charles Stewart at Fri, 2010-04-16 08:47 | login or register to post comments

A rather different reading

I agree with you, but wonder if marco's 'this' referred to your preceeding post or his post to follow.

By Matt M at Fri, 2010-04-16 12:23 | login or register to post comments

Ah, oh, I see

Yes, you're right.

Well, it was probably worth saying why this topic is significant. Apologies to marco for my slow-wittedness.

By Charles Stewart at Fri, 2010-04-16 14:45 | login or register to post comments