Plutusfest

Plutus is the smart contract language for Cardano, the proof-of-work blockchain developed by IOHK. It is based on Haskell, and developed by a team led by Manuel Chakravarty and myself. IOHK will be premiering Plutus to the world at Plutusfest in Edinburgh, this coming Tuesday. You are invited! Details at plutusfest.io.

Brexit: Leave ‘very likely’ won EU referendum due to illegal overspending, says Oxford professor’s evidence to High Court

There's been little attention paid to the fact Vote Leave broke UK spending law. If that had happened in an election to Parliament, the vote would have been annulled and the election held again. I have to admit, despite the breach, I thought it unlikely the extra spending could actually have swung the election. But the Independent reports that Prof Philip Howard of Oxford (above) says otherwise.

[T]he Remain campaign was forced to stop its digital advertising on the last day of the June 2016 campaign because it had reached its spending limit. In contrast, Vote Leave carried on, despite busting its limit two days before the vote – and was later found by the Electoral Commission to have broken the law.

The illegal adverts were seen by millions, of whom 20--30% made up their mind in the last week, and half of those on the last day. In that context, the estimate that 800K people were swayed, more than the 635K needed to change the outcome, seems entirely plausible.

Programming Language Foundations in Agda

Wen Kokke and I are pleased to announce the availability of the textbook:

  Programming Language Foundations in Agda
  plfa.inf.ed.ac.uk
  github.com/plfa/plfa.github.io/

It is written as a literate script in Agda, and available at the above URLs. The books has so far been used for teaching at the Universities of Edinburgh and Vermont, and at Google Seattle. Please send your comments and pull requests!

The book was presented in a paper (of the same title) at the XXI Brazilian Symposium on Formal Methods, 28--30 Nov 2018, and is available here:

  http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf

The paper won the SBMF 2018 Best Paper Award, 1st Place.

Co-Recursive Interview

Adam Gordon Bell interviewed me for his Co-Recursive podcast. Thanks, Adam!

Developer Yoga

My favourite is the first, Lambdasana. Spotted while at LambdUp in Prague.

A new EU law could end the web as we know it (redux)

In June, the EU avoided voting for Articles 11 and 13, which have the potential to end the web as we know it. Now they're back; the vote is 12 September. Up to date info is at Creative Commons, links to help you write, call or tweet are at SaveYourInternet.eu. Below is what I wrote to my MEPs. If you are an EU citizen, you should write too; WriteToThem makes it easy.

Dear Nosheena Mobarik, Alyn Smith, Ian Hudghton, Catherine Stihler, David Martin, and David Coburn,

I write to you greatly disturbed by the new proposals for copyright. These would require any service provider to maintain large, expensive, and ineffective filters. While YouTube, Twitter, or Facebook will have no problems funding these, they will prevent the next innovative service from getting off the ground. Experience with such filters show that they ban all sort of material which should be in the public domain or which is fair use.

I am also concerned by the resurrection of the "link tax". Previous experience with adding a link tax in Germany and Spain showed that the newspapers that requested it soon stopped using it. It is particularly worrying that the legal formulation chosen will invalidate Creative Commons licenses. Many academic journals (including the one which I edit) depend crucially on Creative Commons, and passing a law that invalidates it is against the public interest.

An excellent one-page summary of the issues, with further links, can be found here:

https://boingboing.net/2018/04/11/evidence-free-zone.html

The web has been a huge boon to innovation, creativity, cooperation, and scientific progress. Please don't kill the goose that lays the golden eggs.

Yours sincerely,



Philip Wadler
Professor of Theoretical Computer Science
University of Edinburgh

Why Technology Favors Tyranny

A thoughtful article by Yuval Noah Harari in The Atlantic. Anyone working in computing should be considering the issues raised.

[A]s AI continues to improve, even jobs that demand high intelligence and creativity might gradually disappear. The world of chess serves as an example of where things might be heading. For several years after IBM’s computer Deep Blue defeated Garry Kasparov in 1997, human chess players still flourished; AI was used to train human prodigies, and teams composed of humans plus computers proved superior to computers playing alone.

Yet in recent years, computers have become so good at playing chess that their human collaborators have lost their value and might soon become entirely irrelevant. On December 6, 2017, another crucial milestone was reached when Google’s AlphaZero program defeated the Stockfish 8 program. Stockfish 8 had won a world computer chess championship in 2016. It had access to centuries of accumulated human experience in chess, as well as decades of computer experience. By contrast, AlphaZero had not been taught any chess strategies by its human creators—not even standard openings. Rather, it used the latest machine-learning principles to teach itself chess by playing against itself. Nevertheless, out of 100 games that the novice AlphaZero played against Stockfish 8, AlphaZero won 28 and tied 72—it didn’t lose once. Since AlphaZero had learned nothing from any human, many of its winning moves and strategies seemed unconventional to the human eye. They could be described as creative, if not downright genius.

Can you guess how long AlphaZero spent learning chess from scratch, preparing for the match against Stockfish 8, and developing its genius instincts? Four hours. For centuries, chess was considered one of the crowning glories of human intelligence. AlphaZero went from utter ignorance to creative mastery in four hours, without the help of any human guide.

Based on a True Story

How much of a movie "based on a true story" is actually true? Here is the answer for seventeen movies, ranging from 41% to 100% true. Spotted by Simon Fowler.

Update: the original graph comes from Information is Beautiful.

I'll be speaking at Lambdup 2018 in Prague

I'm looking forward to LambdUp, Prague, 13 September 2018. The programme is up!  My keynote will be the talk below.

Categories for the Working Hacker

The talk will explain why category theory is of interest for developers, taking examples from Java and Haskell, and referencing the new blockchain scripting languages Simplicity, Michelson, and Plutus. The principle of Propositions as Types describes a correspondence between, on the one hand, propositions and proofs in logic, and, on the other, types and programs in computing. And, on the third hand, we have category theory! Assuming only high school maths, the talk will explain how categories model three basic data types: products (logical and), sums (logical or), and functions (logical implication). And it explains why you already learned the most important stuff in high school.

Deacti-Day

I'm a bit late, but I find the arguments in this article compelling. Bye Twitter! I've enjoyed the people, but not the time wasted.

Is the staggeringly profitable business of scientific publishing bad for science?

A long read in the Guardian by Stephen Buranyi.

It is an industry like no other, with profit margins to rival Google – and it was created by one of Britain’s most notorious tycoons: Robert Maxwell.

Spotted by Ross Anderson.

Lambda Days Research Track

CFP for the Lambda Days Research Track is out. Please submit!

A new EU law could end the web as we know it

Laws concerning copyright filters (Article 13) and link tax (Article 11) have been passed the committee stage and are about to be voted on by the entire European Parliament. While some results of EU legislation, such as GDPR, are largely to the good, these new laws are a disaster. They could end the web as we know it.

Below is what I wrote to my MEPs. If you are an EU citizen, you should write too; WriteToThem makes it easy.

Dear Nosheena Mobarik, Alyn Smith, Ian Hudghton, Catherine Stihler, David Martin, and David Coburn,

I write to you greatly disturbed by the new proposals for copyright. These would require any service provider to maintain large, expensive, and ineffective filters. While YouTube, Twitter, or Facebook will have no problems funding these, they will prevent the next innovative service from getting off the ground. Experience with such filters show that they ban all sort of material which should be in the public domain or which is fair use.

I am also concerned by the resurrection of the "link tax". Previous experience with adding a link tax in Germany and Spain showed that the newspapers that requested it soon stopped using it. It is particularly worrying that the legal formulation chosen will invalidate Creative Commons licenses. Many academic journals (including the one which I edit) depend crucially on Creative Commons, and passing a law that invalidates it is against the public interest.

An excellent one-page summary of the issues, with further links, can be found here:

  https://boingboing.net/2018/04/11/evidence-free-zone.html

The web has been a huge boon to innovation, creativity, cooperation, and scientific progress. Please don't kill the goose that lays the golden eggs.

Yours sincerely,



Philip Wadler
Professor of Theoretical Computer Science
University of Edinburgh

Journal of Financial Technology

I've just been appointed to the editorial board of the newly formed Journal of Financial Technology. Please submit! Our second issue will be a special issue devoted to formal methods.

One simple step to increase diversity

One simple step to increase diversity is to ask. From now on, I plan to send all relevant job announcements to Lambda Ladies, specifically by email to the moderators. Above is the Lambda Ladies party at Strange Loop, September 2014. Thank you for existing, ladies!

IOHK is hiring six PLT engineers

IOHK is hiring six Programming Language Theory engineers, to design and implement the smart contract language Plutus and related domain specific languages. Designing scripting languages for smart contracts is a challenging topic, as it is crucial to avoid the sort of exploits that regularly drain Ethereum of tens of millions of dollars worth of cryptocurrency. I am one of the lead designers; two others are Duncan Coutts and Manuel Chakravarty, who are well known to many in this community.

IOHK is one of the leading cryptocurrency firms. Much of its software is implemented in Haskell. All work is open source and publication is encouraged. Indeed, IOHK is unique in that it is committed to basing its development on peer-reviewed research, in cryptography and security as well as in programming languages and formal methods. As Charles Hoskinson, IOHK's CEO, points out, if IOHK succeeds it may impact how software is developed, encouraging others to more seriously consider functional programming, formal methods, and peer-review. IOHK is a distributed company: I am in Edinburgh and Rio de Janeiro; Duncan is in London; Manuel is in Sydney; you may work from wherever you like.

Further details here:
  https://iohk.io/careers/#op-235152-functional-compiler-engineer-