Wadler's Blog

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.

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

Simplicity

Only once in my life have I encountered a programming language that was too simple to use. That was Lispkit Lisp, developed by Peter Henderson, Geraint Jones, and Simon Jones, which I saw while serving as a postdoc at Oxford, 1983–87, and which despite its simplicity was used to implement an entire operating system. It is an indightment of the field of programming languages that I have not since encountered another system that I consider too simple. Until today. I can now add a second system to the list of those that are too simple, the appropriately-titled Simplicity, developed by Russell O'Connor of Blockstream. It is described by a paper here and a website here.
The core of Simplicity consists of just nine combinators: three for products (pair, take, and drop), three for sums (injl, injr, and case), one for unit (unit), and two for plumbing (iden and comp). It is throughly grounded in ideas from the functional programming, programming language, and formal methods communities.
When I call Simplicity too simple it is intended as a compliment. It is delightful to see full adders and cryptographic hash functions cobbled together using just products, sums, and units. It is eye-opening to see how far one can get without recursion or iteration, and how this enables simple analyses of the time and space required to execute a program. It is a confirmation to see a system with foundations in category theory and sequent calculus. Now I know what to say when developers respond to my talk "Categories for the Working Hacker" by asking "But how can we use this in practice?"
The system is accompanied by a proof of its correctness in Coq, which sets a high bar for competing systems. O'Connor even claims to have a proof in Coq that the Simplicity implementation of SHA-256 matches the reference specification provided by Andrew Appel's Verified Software Toolchain project (VST), which VST proved corresponds to the OpenSSL implementation of SHA-256 in C.
At IOHK, I have been involved in the design of Plutus Core, our own smart contract scripting language, working with Darryl McAdams, Duncan Coutts, Simon Thompson, Pablo Lamela Seijas, and Grigore Rosu and his semantics team. We have a formal specification which we are preparing for release. O'Connor's work on Simplicity has caused us to rethink our own work: what can we do to make it simpler? Thank you, Russell!
That said, Simplicity is still too simple, and despite its emphasis on rigour there are some gaps in its description.

Jets

A 256-bit full adder is expressed with 27,348 combinators, meaning addition in Simplicity requires several orders of magnitude more work than the four 64-bit addition instructions one would normally use. Simplicity proposes a solution: any commonly used sequence of instructions may be abbreviated as a "jet", and implemented in any equivalent matter. Hence, the 27,348 combinators for the 256-bit full adder can be ignored, and replaced by the equivalent four 64-bit additions.
All well and good, but this is where it gets too simple. No one can afford to be inefficient by several orders of magnitude. Hence, any programmer will need to know what jets exist and to exploit them whenever possible. In this sense, Simplicity is misleadingly simple. It would be clearer and cleaner to define each jet as an opcode. Each opcode could still be specified by its equivalent in the other combinators of Simplicity, but programs would be more compact, faster to execute, and—most important—easier to read, understand, and analyse accurately. If one ignores jets, the analyses of time and space required to execute a program, given toward the end of the paper, will be useless—off by orders of magnitude. The list of defined jets is given nowhere in the paper. Nor could I spot additional information on Simplicity linked to from its web page or findable by a web search. More needs to be done before Simplicity can be used in practice.

Gaps

It's not just the definition of jets which is absent from the paper, and cannot be found elsewhere on the web. Lots more remains to be supplied.

• Sections 2.4, 2.5, 3.2 claim proofs in Coq, but apart from defining the semantics of the nine combinators in Appendix A, no Coq code is available for scrutiny.
• Section 2.5 claims a representation of Simplicity terms as a dag, but it is not specified. Lacking this, there is no standard way to exchange code written in Simplicity.
• Section 4.4 defines an extended semantics for Simplicity that can read the signature of the current transaction, support Merklised abstract syntax trees, and fail when a transaction does not validate. It also lifts meanings of core (unextended) Simplicity programs to the extended semantics. However, it says nothing about how the seven combinators that combine smaller Simplicity programs into bigger ones act in the extended semantics! It's not hard to guess the intended definitions, but worrying that they were omitted from a paper that aims for rigour.
• Section 3 provides a Bit Machine to model the space and time required to execute Simplicity. The model is of limited use, since it ignores the several orders of magnitude improvement offered by jets. Further, the Bit Machine has ten instructions, enumerated on pages 10–12, but the list omits the vital "case" instruction which appears in Figure 2. Again, it's not hard to guess, but worrying it was omitted.

Michelson

A second language for scripting blockchains is Michelson. It is described by a paper here and a website here. (Oddly, the website fails to link to the paper.)
I will offer just one word on Michelson. The word is: "Why?"
Michelson takes many ideas from the functional programming community, including higher-order functions, data structures such as lists and maps, and static type safety. Currently, it is also much more thoroughly described and documented than Simplicity. All of this is to be commended.
But Michelson is an inexplicably low-level language, requiring the programmer to explicitly manipulate a stack. Perhaps this was done so that there is an obvious machine model, but Simplicity offers a far superior solution: a high-level model for programming, which compiles to a low-level model (the Bit Machine) to explicate time and space costs.
Or perhaps Michelson is low-level to improve efficiency. Most of the cost of evaluating a smart contract is in cryptographic primitives. The rest is cheap, whether compiled or interpreted. Saving a few pennies of electricity by adopting an error prone language—where there is a risk of losing millions of dollars in an exploit—is a false economy indeed. Premature optimisation is the root of all evil.
The language looks a bit like all the bad parts of Forth and Lisp, without the unity that makes each of those languages a classic. Lisp idioms such as CAAR and CDADAR are retained, with new ones like DUUP, DIIIIP, and PAAIAIAAIR thrown in.
There is a fair set of built-in datatypes, including strings, signed and unsigned integers, unit, product, sum, options, lists, sets, maps, and higher-order functions. But there is no way for users to define their own data types. There is no way to name a variable or a routine; everything must be accessed by navigating a data structure on the stack.
Some operations are specified formally, but others are left informal. For lists, we are given formal rewriting rules for the first three operators (CONS, NIL, IF_CONS) but not the last two (MAP, REDUCE). Type rules are given in detail, but the process of type inference is not described, leaving me with some questions about which programs are well typed and which are not. It reminds me of a standard problem one sees in early work by students—the easy parts are thoroughly described, but the hard parts are glossed over.
If I have understood correctly, the inference rules assign types that are monomorphic, meaning each term has exactly one type. This omits one of the most successful ideas in functional programming, polymorphic routines that act on many types. It means back to the bad old days of Pascal, where one has to write one routine to sort a list of integers and a different routine to sort a list of strings.
Several of these shortcomings are also shared by Simplicity. But whereas Simplicity is intended as a compilation target, not to be read by humans, the Michelson documentation includes a large collection of examples suggesting it is intended for humans to write and read.
Here is one of the simpler examples from the paper.

  { DUP ; CDAAR ; # T
    NOW ;
    COMPARE ; LE ;
    IF { DUP ; CDADR ; # N
         BALANCE ;
         COMPARE ; LE ;
         IF { CDR ; UNIT ; PAIR }
            { DUP ; CDDDR ; # B
              BALANCE ; UNIT ;
              DIIIP { CDR } ;
              TRANSFER_TOKENS ;
              PAIR } }
       { DUP ; CDDAR ; # A
         BALANCE ;
         UNIT ;
         DIIIP { CDR } ;
         TRANSFER_TOKENS ;
         PAIR } }

The comment # T is inserted as a reminder that CDAAR extracts variable T, and similarly for the other variables N, B, and A. This isn't the 1950s. Why don't we write T when we mean T, instead of CDAAR? WHY ARE WE WRITING IN ALL CAPS?
In short, Michelson is a bizarre mix of some of the best and worst of computing.

Conclusion

It is exciting to see ideas from the functional programming, programming languages, and formal methods communities gaining traction among cryptocurrencies and blockchains. While there are shortcomings, it is fantastic to see an appreciation of how these techniques can be applied to increase reliability—something which the multi-million dollar exploits against Ethereum show is badly needed. I look forward to participating in the conversations that ensue!

Postscript

The conversation has begun! Tezos have put up a page to explain Why Michelson. I've also learned there is a higher-level language intended to compile into Michelson, called Liquidity.

Labels: Blockchain, Functional Programming, Programming Languages

Humble Book Bundle is selling off a passle of Java books, including Java Generics and Collection by Naftalin and Wadler, on a pay-what-you-want basis (USD $1 minimum), DRM-free. You choose what proportion of the profits go to Humble and what goes to the charity Code for America. A great deal!

Labels: Developers, DRM, Java, Programming Languages

Today is an internet-wide day of action to support Net Neutrality.

Net Neutrality is under severe attack by the FCC and the Trump Administration. Only sustained action will save it. And if it falls in the US, will it be long before the rest of the world follows?

Net Neutrality is already being eroded. Virgin proudly tells me that I'm not charged mobile bandwidth when I use Twitter; other providers offer similar services for Facebook or Netflix. Seemingly a bonus, these offers are really a minus: they lock in the present winners, and make it difficult for the next generation of innovations to emerge.

Unless we act now, people will look back on our days as 'The Golden Age of the Internet'.

Do something now! It takes less than ten minutes. Details here.

Labels: Internet, Net Neutrality, Politics, US, Web

Proceedings of the ACM on Programming Languages (PACMPL) is a new, open-access journal that will archive the results of major programming language conferences sponsored by SIGPLAN and ACM. So far, ICFP, OOPSLA, and POPL have signed on. There is, to my surprise, a raging debate as to whether PLDI should do so. The issues are blogged here, and there is a survey here.

As Editor-in-Chief of PACMPL, I may be prejudiced, but it seems to me the case for PLDI to join is a no-brainer.  Programming languages are unusual in a heavy reliance on conferences over journals. In many universities and to many national funding bodies, journal publications are the only ones that count. Other fields within computing are sorting this out by moving to journals; we should too. Journals cover a wide range of different publications, and our better conferences sit toward the high-quality end of this range. ICFP, OOPSLA, and POPL were all enthusiastic to join; is PLDI that different?

Becoming a journal requires a slight change to procedure: an extra round for referees to ensure necessary changes have been made. The extra round increases reliability of our archival publication—good, as we don't want to build our field on sand!—and may permit the PC to be more adventurous in accepting borderline papers.

Most importantly, all papers in PACMPL will be open access, thanks to generous underwriting by SIGPLAN. The price ACM is charging is too high, and we will continue to press them to reduce it. But it is only by going to open access that SIGPLAN can survive—the alternative is that our conferences, including PLDI, will wither, to be replaced by others that are open access.

I urge you to fill out the survey, as it is your opinion that could tilt the balance. Though the survey is non-binding, it will powerfully influence the PLDI Steering Committee when they vote on the issue next month. It just takes a minute, do it now!

Labels: ACM, Open Access, Programming Languages, SIGPLAN

 DSLDI 2017, colocated with SPLASH in Vancouver, October 2017.
Please submit to

DSLDI is a single-day workshop and will consist of an invited speaker followed by moderated audience discussions structured around a series of short talks. The role of the talks is to facilitate interesting and substantive discussion. Therefore, we welcome and encourage talks that express strong opinions, describe open problems, propose new research directions, and report on early research in progress.
Proposed talks should be on topics within DSLDI’s area of interest, which include but are not limited to:

• solicitation and representation of domain knowledge

• DSL design principles and processes

• DSL implementation techniques and language workbenches

• domain-specific optimizations

• human factors of DSLs

• tool support for DSL users

• community and educational support for DSL users

• applications of DSLs to existing and emerging domains

• studies of usability, performance, or other benefits of DSLs

• experience reports of DSLs deployed in practice

Labels: DSL, Programming Languages

Please submit to RADICAL 2017, Recent Advances in Concurrency and Logic, a workshop co-located with QONFEST (CONCUR, QEST, FORMATS, and EPEW), Berlin (Germany), September 4, 2017.

As you know, submissions to RADICAL could be, for instance:- reports of an ongoing work and/or preliminary results;- summaries of an already published paper (even at CONCUR'17 - see below);- overviews of (recent) PhD theses;- descriptions of research projects and consortia;- manifestos, calls to action, personal views on current and future challenges;- overviews of interesting yet underrepresented problems.
...
Many thanks for your cooperation!Julian and Jorge

Labels: Concurrency, Logic, Programming Languages

Leave it to George Monbiot to make the most effective case for Labour.

On policy after policy, the Labour manifestoaccords with what people say they want. It offers a strong and stable National Health Service, in which privatisation is reversed, clinical budgets rise and staff are properly paid. It promises more investment in schools, smaller class sizes, and an end to the stifling micromanagement driving teachers out of the profession. It will restore free education at universities. It will ensure that railways, water, energy and the postal service are owned for the benefit of everyone, rather than only the bosses and shareholders. It will smoke out tax avoidance, and bring the banks under control.
While Theresa May will use Brexit as a wrecking ball to be swung at workers’ rights, environmental laws and other regulations the Conservative party has long wanted to destroy, Labour has promised to enhance these public protections. It will ban zero-hours contracts, prevent companies from forcing their staff into bogus self-employment, and give all workers – whether temporary or permanent – equal rights. The unemployed will be treated with respect. Both carers and people with disabilities will be properly supported. Those who need homes will find them, and tenants will be protected from the new generation of rack-renting slumlords. Who, apart from the richest beneficiaries of the current regime, would not wish to live in such a nation?  ...

[May] won’t stand up to anyone who wields power. She will say nothing against Donald Trump, even when he peddles blatant falsehoods in the aftermath of terrorist attacks in this nation, exploiting our grief to support his disgusting prejudices; even when he pulls out of the global agreement on climate change.
She is even more sycophantic towards this revolting man than Tony Blair was to George W Bush. She won’t confront Saudi Arabia over terrorism or Yemen or anything else. ...
She won’t stand up to the polluters lavishly funding the Conservative party, whose role explains both her weakness on climate change and her miserable failure to address our air pollution crisis. She won’t stand up to the fanatics in her party who call for the hardest of possible Brexits. She won’t stand up on television to debate these policies because she knows that the more we see, the less we like. The party machine’s attempt to build a personality cult around her fell at an obvious hurdle: first, you need a personality.  ...

The election now hangs on whether the young people who claim they will vote Labour are prepared to act on this intention. We know that older Conservative voters will make good their promise: they always do. Will the young electors, who will lose most from another five years of unresponsive government, walk a couple of hundred metres to their polling stations? Or will they let this unprecedented chance to change the nation slip through their fingers? The world belongs to those who turn up.

Labels: Politics, UK

The death on Wednesday (31st May) of a young woman in Edinburgh on Wednesday has hit a nerve with cyclists across Scotland. She appears to have been killed after her bike slipped on the tram tracks on Princes Street.
Edinburgh’s tram tracks have been described as an accident waiting to happen from the moment they were unveiled. [H]undreds of cyclists have been injured from falls on the tracks, and thousands more have had close shaves. This Wednesday (7th June), at 8:30 am, cyclists in Edinburgh will be marking Zhi Min Soh’s death. There will be a short, respectful protest at the junction where she died, reflecting the emotion that has bubbled up in the days since this senseless death. Although we are not organising it, we fully support this action and ask anyone who can to come and join them, on bike or on foot, and whether you cycle or not.If you can attend, please make your way directly to Shandwick Place for 8:30 a.m. If you can, bring a sign or a placard letting people know what it is about. People will gather at the junction for a minute’s silence, and a lament from a piper to remember this death, and to ask for the City of Edinburgh to take action to ensure that it will be the last.

Labels: Cycling, Edinburgh

I suggested a team-up, and, lo, it appears!

Labels: Category Theory, Functional Programming, Haskell

I was delighted and gobsmacked to hear from Moises Vazquez, a university teacher from Mexico who has a penchant for dressing up as Spider-Man. Reuters reports:

"I do the same job as anyone else, I don't think it's the best class in the world just because I put on a suit. But I assure you I want to be the most honest and dedicated there is, I just want to make the classroom a better place," he said.

I am blown away by his costume, with amazing detail such as Barendregt's lambda cube on the back and categorical arrows for webbing. Time for a superhero team-up?

Labels: Category Theory, Functional Programming, Haskell

As the creators put it

Explained Visually (EV) is an experiment in making hard ideas intuitive inspired the work of Bret Victor's Explorable Explanations. Sign up to hear about the latest.

I've found their explanations of Markov Chains and Eigenvectors and Eigenvalues both cool and clear.

Labels: Graphics, Mathematics

I suggested at Papers We Love that someone might like to recode John Reynolds's definitional interpeter, and I'm pleased to say that Rein Henrichs has done so.

Labels: Functional Programming, Haskell, Programming Languages

Two years ago we lost Paul Hudak to cancer. Today I was saddened to learn that we have lost his close collaborator, John Peterson, to a climbing accident. Both will be missed.

Labels: Functional Programming, Haskell

Tomorrow Edinburgh City Council will decide between Options A and B for the East-West Cycle route, after deferring a decision last September.  Some of the recent coverage:

• A visualisation of Roseburn Option A (above).
• A comparison of road layout, current against Option A (below).
• A letter in the Edinburgh Evening News from East-West nemesis Pete Gregson.
• A letter from Transport Committee head Leslie Hinds, rebutting the previous letter.
• A two-page spread in the Edinburgh Evening News.
• A blog post from Daisy Narayanan of Sustrans.

Daisy's post hit the mark:

We have seen narratives that create an ‘us’ and ‘them’ – pitting ‘motorists’ against ‘cyclists’ against ‘pedestrians’. With such projects, it is hugely disheartening to see what should have been a force for positive change become a focus for anger. It is equally disheartening to see strong evidence and the policies of the Scottish Government which support a more active, greener Scotland being undermined by such opposition.

In darker moments, I have been tempted to draw parallels to the post-fact world that we seem to inhabit at present.

  Option A: Think about the children

Labels: Cycling, Edinburgh, Politics