Lambda the Ultimate

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!

Thanks, I didn't know about this!

Haskell video lectures online

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

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.

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!

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?

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.

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.

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.

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?

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?

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

Yes, you're right.

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