Wadler's Blog

Courtesy of Tom The Dancing Bug.

Labels: Comics, Covid-19

Thank you, XKCD!

Labels: Comics, Covid-19

An intriguing essay by Philip J. David and Reuben Hirsch.

The ideal mathematician’s work is intelligible only to a small group of specialists, numbering a few dozen or at most a few hundred. This group has existed only for a few decades, and there is every possibility that it may become extinct in another few decades. However, the mathematician regards his work as part of the very structure of the world, containing truths which are valid forever, from the beginning of time, even in the most remote corner of the universe.

Labels: Academia, Mathematics

For my final year project I’ve build an interactive fractal viewer using WebAssembly and Web Workers to create a multithreaded renderer. You can try it now mmaps.freddiejbawden.com! Feedback can be left at mmaps.freddiejbawden.com/feedback and is greatly appreciated. Thanks!

Labels: Computing, Graphics, JavaScript, Mathematics, Web

Unclear on what is happening with Coronavirus or what you should do about it? Tomas Pueyo presents a stunning analysis with lots of charts, a computer model you can use, and some clear and evidence-based conclusions. Please read it and do as he says!

Labels: Academia, Politics, Scotland

One of my honours project students, Joao Maio, has done a great job with an update to Mandelbrot Maps. He's looking for feedback. Try it out!

I'm looking for feedback for an app that I've developed for my honours project - an interactive fractal explorer called Mandelbrot Maps! It is built with React and WebGL, and has a simple and intuitive user interface. 
Try it out at https://jmaio.github.io/mandelbrot-maps/ - please leave your feedback through the button on the website ([Settings] > [Info] > [Feedback]).

Labels: Computing, Graphics, JavaScript, Mathematics, Web

There has been much discussion of how to reduce the carbon footprint of conferences by supporting remote attendance in real time, now accelerated by the advent of coronavirus.

Most of the models I've seen discussed are synchronous, supporting virtual attendance in real-time. I was intrigued by this white paper, which proposes an asynchronous model. Talks are grouped into sessions of three, with Q&A panels open for comment for a period of a few weeks.

On average, the pilot conferences’ Q&A sessions generated three times more discussion than takes place at a traditional Q&A. A few sessions generated more than ten or fifteen times more, making clear that, while different from a traditional conference, meaningful personal interaction was not only possible, but in certain respects superior.

Labels: Academia, Climate Change, Politics

My attempt to explain Propositions as Types to a general audience. Recorded at Bright Club, The Stand, Edinburgh, 23 September 2019.

Labels: Comedy, Functional Programming, Logic, Programming Languages, Types

• Practical systems verification: e.g. for operating systems, databases, compilers, distributed systems
• Language-based verification: static analysis, verified systems / smart contract programming, types, SAT/SMT solving
• Engineering trustworthy software: automated/property-based testing, bug finding, dynamic instrumentation, runtime verification

Labels: Academia, Computing, Edinburgh, Formal Methods, Functional Programming, Programming Languages

In the run-up to the election, I am passing on a couple of resources in case readers find them of value.

Antisemitism has been so much in the news that everyone must believe there cannot be smoke without fire. But if you dig into the allegations, it becomes clear that a minuscule flame has been fanned for political purposes.

How Labour Became “Antisemitic”

Ever since his shock election to the Labour leadership in 2015, Jeremy Corbyn has been dogged by allegations of “antisemitism.” Both the media and hostile MPs claim he has failed to confront Jew-hate in party ranks — one Tory minister even said Corbyn would be “the first antisemitic Western leader since 1945.” Often bound up with debates on Israel and anti-imperialism, this has become one of the main lines of attack against Corbyn, both within and outside the party.
Yet for all the headlines about “mounting antisemitism” in Labour, we are rarely given any sense of its scale. Data released by the party in February 2019 showed that it had received 1,106 specific complaints of antisemitism since April 2018, of which just 673 regarded actual Labour members. The party membership stands at over half a million: the allegations, even if they were true, concern around 0.1 percent of the total.
Constant media talk of Labour’s “antisemitism crisis” has nonetheless warped all discussion of this issue. This is a key finding of Bad News for Labour, a new book on the party’s handling of antisemitism claims. The study is especially notable for its use of focus groups and polling to gauge public perceptions of the affair: when its authors commissioned Survation to ask 1,009 people how many Labour members faced antisemitism complaints, the average estimate — at 34 percent — was over three hundred times the published figures.

Labels: Politics

In the run-up to the election, I am passing on a couple of resources in case readers find them of value.

Must watch film - now offered free in time for General Election 2019.

The Great NHS Heist forensically examines not only how the Tories plan to sell off the NHS but how they are already well advanced in smashing it apart, selling off the fragments piece by piece.

Labels: Politics

Caitlin Kirby, a graduate student in earth and environment science at Michigan State University, defended her doctoral dissertation while wearing a skirt she had made from 17 rejection letters she had received in the course of her studies.

“The whole process of revisiting those old letters and making that skirt sort of reminded me that you have to apply to a lot of things to succeed,” she said. “A natural part of the process is to get rejected along the way.” ... "I just searched for 'unfortunately' and 'we regret to inform you' in my email"

Spotted via Boing Boing.

Labels: Academia

How Amazon Web Services Uses Formal Methods by Newcombe et al, appeared in Communications of the ACM in April 2015. It describes the use of Leslie Lamport's TLA+ (Temporal Logic of Actions) to refine the design of web services such as Dynamo DB and S3. (S3 stored 2 billion objects and handled 1.1 million transaction per second back in 2013.) Thanks to Jessica Kerr for pointing me to this paper after an interview for the podcast Greater Than Code.

We find a major benefit of having a precise, testable model of the core system is that we can quickly verify that even deep changes are safe or learn they are unsafe without doing harm. In several cases, we have prevented subtle but serious bugs from reaching production. In other cases we have been able to make innovative performance optimizations (such as removing or narrowing locks or weakening constraints on message ordering) we would not have dared to do without having model-checked those changes. A precise, testable description of a system becomes a what-if tool for designs, analogous to how spreadsheets are a what-if tool for financial models. We find that using such a tool to explore the behavior of the system can improve the designer’s understanding of the system.

Labels: Computing, Concurrency, Formal Methods, Programming Languages

The Next 7000 Programming Languages, by Chatley, Donaldson, and Mycroft, appears in a book marking 10,000 volumes of LNCS. Though they riff on Landin's title, the authors consider something quite different: Darwinian evolution in the context of programming languages. I've long thought we need a theory of the economics of programming languages, to explain why the most popular language is not always that one might consider best suited to a task. But, until now, it's not been clear to me what such a theory might consist of, other than the observation that network effects apply to programming languages. This paper points in the direction of a theory of programming languages as a whole, drawing on evolutionary theory and with a potential grounding in empirical measures, such as scraping Github to measure which languages are more or less popular.

It is useful here to distinguish between the success of a species of plant (or a programming language) and that of a gene (or programming language concept). For example, while pure functional languages such as Haskell have been successful in certain programming niches the idea (gene) of passing side-effect-free functions to map, reduce, and similar operators for data processing, has recently been acquired by many mainstream programming languages and systems; we later ascribe this partly to the emergence of multi-core processors.

This last example highlights perhaps the most pervasive form of competition for niches (and for languages, or plants, to evolve in response): climate change. Ecologically, an area becoming warmer or drier might enable previously non-competitive species to get a foothold. Similarly, even though a given programming task has not changed, we can see changes in available hardware and infrastructure as a form of climate change—what might be a great language for solving a programming problem on a single-core processor may be much less suitable for multi-core processors or data-centre solutions.

Amusingly, other factors which encourage language adoption (e.g. libraries, tools, etc.) have a plant analogy as symbiotes—porting (or creating) a wide variety of libraries for a language enhances its prospects.

Labels: Dynamic and Static Typing, Functional Programming, Programming Languages, Science

At Haskell Exchange, Stephan Schneider introduced me to Toki Pona, an extremely simple artificial language, based on 120 symbols. You can read more on Wikipedia.

Labels: Logic, Writing

Fly, drive, train? Here's a resource to help you decide. Spotted by Michael J. Oghia of the ACM Climate group.

Labels: Climate Change, Politics

The Plutus team at IOHK is headed by Manuel Chakravarty and consists of a small but strong team of developers; I work on it as a consultant. We are designing a smart contract language, based on Haskell (for both offchain and onchain user-level programming) and System F (as the core code that runs onchain, the equivalent of the EVM for Ethereum). IOHK, unlike any other firm I know, is committed to building on peer-reviewed research, so publication is encouraged. We are hiring!

As a Functional Compiler Engineer at IOHK you will work closely with our programming language theory and cryptography researchers, our formal methods team, and our engineering team throughout the smart contracts development programme involving design, coding, testing and integrating of new smart scripting languages into our blockchain technology. This also includes the design and implementation of relevant domain specific languages (DSLs). You will have a strong understanding of programming language design, type systems, operational semantics, interpreters, and compiler implementation techniques.

Applications from folk who will increase our diversity are encouraged. Details here.

Labels: Blockchain, Functional Programming, Haskell, IOHK

If you are a UK citizen, please remember to vote in the EU elections tomorrow. Latest poll results for Scotland from the Herald are above (and linked). I will vote Green.

Farage's Brexit Party is doing distressingly well. If you are considering sitting this one out, I remind you of the words of Robert Heinlein:

If you are part of a society that votes, then do so. There may be no candidates and no measures you want to vote for ... but there are certain to be ones you want to vote against. [from Time Enough for Love]

Labels: EU, Politics, Scotland

Next week, I will teach six hours of classes based on PLFA, and deliver a departmental seminar on the same topic. Maybe I will see you there!

Seminar: 16.00-17.00 Tue 28 May (details)

Classes: 12.30-15.30 Wed-Thu 29-30 May (details)

Labels: Agda, Education, Functional Programming, Types

Steven Pinker tweets thirteen rules for better writing. Spotted via Boing Boing.

1. Reverse-engineer what you read. If it feels like good writing, what makes it good? If it’s awful, why?
2. Prose is a window onto the world. Let your readers see what you are seeing by using visual, concrete language.
3. Don’t go meta. Minimize concepts about concepts, like “approach, assumption, concept, condition, context, framework, issue, level, model, perspective, process, range, role, strategy, tendency,” and “variable.”
4. Let verbs be verbs. “Appear,” not “make an appearance.”
5. Beware of the Curse of Knowledge: when you know something, it’s hard to imagine what it’s like not to know it. Minimize acronyms & technical terms. Use “for example” liberally. Show a draft around, & prepare to learn that what’s obvious to you may not be obvious to anyone else.
6. Omit needless words (Will Strunk was right about this).
7. Avoid clichés like the plague (thanks, William Safire).
8. Old information at the beginning of the sentence, new information at the end.
9. Save the heaviest for last: a complex phrase should go at the end of the sentence.
10. Prose must cohere: readers must know how each sentence is related to the preceding one. If it’s not obvious, use “that is, for example, in general, on the other hand, nevertheless, as a result, because, nonetheless,” or “despite.”
11. Revise several times with the single goal of improving the prose.
12. Read it aloud.
13. Find the best word, which is not always the fanciest word. Consult a dictionary with usage notes, and a thesaurus.

After absorbing these, read his The Sense of Style.

Labels: Education, Writing

I just returned from teaching a class of twenty-two women in Addis Ababa, courtesy of IOHK. Rounding off eight weeks of Haskell, taught by Lars Brünjes and Polina Vinogradova, I spent two weeks teaching IOHK's smart contract languages Plutus and Marlowe. It was an amazing experience. I thank IOHK and my students for the opportunity, and I look forward to repeating it someday.

Here is IOHK's announcement prior to the course, and an analysis from an outsider.

Thank you to my students for introducing me to injera!


With Wanda, Lars, and Polina in traditional dress at the graduation ceremony.

Labels: Blockchain, Haskell, IOHK

Trevor Sumner delivers an incisive analysis of the root causes of the Ethiopian airlines crash. Many call it a software failure, but he looks at a trail of issues: economic problem, airframe problem, aerodynamic problem, systems engineering problem, sensor problem, maintenance practices problem, pilot training problem, pilot expertise problem, and back to economic problem.

(Thanks to Robin Sloan for highlighting Sumner's post in his weekly newsletter, Year of the Meteor.)

Labels: Computing, Technology

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.

Labels: Blockchain, Edinburgh, Haskell

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.

Labels: Brexit, EU, Europe, Politics, UK

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.

Labels: Agda, Functional Programming, Logic, Programming Languages, Types

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

Labels: Computing, Functional Programming, Programming Languages

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

Labels: Developers, Functional Programming

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

Labels: Copyright, Europe, Politics, Web

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.

Labels: Computing, Politics

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.

Labels: Cinema

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.

Labels: Category Theory, Functional Programming

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.

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.

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

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

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.