3.7.20
Haskell, Then and Now. Got Questions? Ask them here!
IOHK Cardano Virtual Summit continues. Today's sessions include:
16.00 Fri 3 Jul Haskell, then and now: What is the future for functional programming languages? Prof Simon Peyton-Jones, Prof John Hughes, Prof Philip Wadler, Dr Kevin Hammond, Dr Duncan Coutts.
You can submit questions via Reddit. Register for the summit here. You can log in with your registered username and password here.
Labels: Blockchain, Cryptocurrency, Functional Programming, Haskell, IOHK
30.6.20
Cardano Virtual Summit 2020
I'm participating in four sessions at Cardano Virtual Summit 2020, and there are many other sessions too. All times UK/BST.
16.00 Thu 2 Jul An overview of IOHK research Prof Aggelos Kiayias, Prof Elias Koutsoupias, Prof Alexander Russell, Prof Phil Wadler.
18.30 Thu 2 Jul Architecting the internet: what I would have done differently... Vint Cerf, Internet pioneer and Google internet evangelist, Prof Aggelos Kiayias, panel moderated by Prof Philip Wadler.
20.00 Thu 2 Jul Functional smart contracts on Cardano Prof Philip Wadler, Dr Manuel Chakravarty, Prof Simon Thompson.
16.00 Fri 3 Jul Haskell, then and now: What is the future for functional programming languages? Prof Simon Peyton-Jones, Prof John Hughes, Prof Philip Wadler, Dr Kevin Hammond, Dr Duncan Coutts.
Labels: Blockchain, Cryptocurrency, Functional Programming, Haskell, IOHK
25.6.20
An Incredible Scientific Breakthrough Discovery to Beat Covid
Labels: Covid-19
16.6.20
Haskell Love
I am speaking at Haskell Love, 31 July--1 August 2020, a virtual event.
Labels: Functional Programming, Haskell
Jared Diamond: Lessons from a Pandemic
Another hopeful analysis, from Jared Diamond, author of Guns, Germs, and Steel, one of my favourite books.
Covid-19 doesn’t represent an existential threat to the survival of our species. Yes, the pandemic will be a serious blow to the world’s economy, but that will recover; it’s only a matter of time. Unlike many of the epidemics of the past, the virus isn’t threatening to cause military defeats, population replacements or crashes, or abandonments of land under cultivation.
There are other dangers, present right now, that do constitute existential threats capable of wiping out our species, or permanently damaging our economy and standard of living. But they are less convincing at motivating us than is Covid-19, because (with one exception) they don’t kill us visibly and quickly.
Strange as it may seem, the successful resolution of the pandemic crisis may motivate us to deal with those bigger issues that we have until now balked at confronting. If the pandemic does at last prepare us to deal with those existential threats, there may be a silver lining to the virus’s black cloud. Among the virus’s consequences, it could prove to be the biggest, the most lasting — and our great cause for hope.
Labels: Covid-19
27.5.20
Kim Stanley Robinson: The Coronavirus Is Rewriting Our Imaginations
One of the more thoughtful and hopeful analyses I've seen, from sf writer Kim Stanley Robinson in The New Yorker.
The critic Raymond Williams once wrote that every historical period has its own “structure of feeling.” How everything seemed in the nineteen-sixties, the way the Victorians understood one another, the chivalry of the Middle Ages, the world view of Tang-dynasty China: each period, Williams thought, had a distinct way of organizing basic human emotions into an overarching cultural system. Each had its own way of experiencing being alive.
In mid-March, in a prior age, I spent a week rafting down the Grand Canyon. When I left for the trip, the United States was still beginning to grapple with the reality of the coronavirus pandemic. Italy was suffering; the N.B.A. had just suspended its season; Tom Hanks had been reported ill. When I hiked back up, on March 19th, it was into a different world. I’ve spent my life writing science-fiction novels that try to convey some of the strangeness of the future. But I was still shocked by how much had changed, and how quickly.
Schools and borders had closed; the governor of California, like governors elsewhere, had asked residents to begin staying at home. But the change that struck me seemed more abstract and internal. It was a change in the way we were looking at things, and it is still ongoing. The virus is rewriting our imaginations. What felt impossible has become thinkable. We’re getting a different sense of our place in history. We know we’re entering a new world, a new era. We seem to be learning our way into a new structure of feeling.
Labels: Covid-19
18.5.20
Flying in the age of Covid 19
Erin Bromage is an immunologist teaching at UMass Dartmouth. He writes a blog aiming to explain what is known about how Covid 19 spreads to the general public. He is most famous for a post detailing what is known about spread of Covid 19 in closed environments. If you may need to travel, his post on flying may prove helpful. (Photo from the Twitter feed of Ethan Weiss, flying United.)
Labels: Covid-19
9.5.20
Who is beating Covid 19?
30.4.20
PhD position in Certifying Compilation of Smart Contracts
This project aims to develop a certifying compiler for Plutus Tx, a subset of the purely functional language Haskell that is used to implement smart contracts for the Cardano blockchain. The Plutus smart contract framework is being developed by IOHK for Cardano and the present project is a joint effort of IOHK and Utrecht University. The Plutus Tx compiler is based on the GHC Haskell compiler and adds a translation step from GHC Core to a minimal lambda calculus. Programmes in this lambda calculus are executed during transaction validation in a sandboxed execution environment in a manner that is crucial to the security of the blockchain. The aim of this project is to formalise the semantics of the languages involved in a proof assistant such as Coq, to reason about the transformation and optimisation steps that the compiler performs, and finally, to generate a proof object certifying the correctness of the generated code together with that code.
Labels: Cryptocurrency, Formal Methods, Functional Programming, Haskell, Theory, Types
28.4.20
Every Proof Assistant
Andrej Bauer writes:
For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.
Getting the authors of proof assistants to travel to Ljubljana and giving talks at our Foundations of mathematics and theoretical computer science seminar has largely become impossible. But luckily research seminars world-wide are rapidly moving online, and so is our Foundations seminar. I am therefore delighted to announce the first "Every proof assistant" seminar. ...
I have a couple more in the pipeline, so follow this blog, the Foundations seminar announcements or my Twitter account @andrejbauer.
Labels: Logic, Mathematics, Types
13.4.20
The Tempest
In many ways, Covid 19 has expanded rather than contracted our cultural opportunities. Today, Wanda and I saw an interactive online live abridged production of The Tempest, from Creation Theatre. It was great! We were lucky to get one of the extra places they added due to demand. They are likely to put on additional shows, keep an eye out. Spotted via The Guardian.
Labels: Covid-19, Technology, Theatre, Web
11.4.20
Virtual Conferences: A Guide to Best Practices
A report from the ACM Presidential Task Force on on What Conferences Can Do to Replace Face-to-Face Meetings. Thank you to Crista Videira Lopes, Jeanna Matthews, Benjamin Pierce, and the other members of the task force.
“Our conference organizing committee just decided to switch our physical conference to online. But the conference is supposed to start in three weeks, and none of us have ever even been to a virtual conference, much less put one on! Where do we start??”
Labels: Academia, ACM, Covid-19, SIGPLAN, Web
3.4.20
The New New Yorker
31.3.20
XKCD vs Coronavirus
17.3.20
The Ideal Mathematician
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
12.3.20
Try out the new Mandelbrot Maps, Part II
Another one of my honours project students, Freddie Bawden, has also done a great job with an update to Mandelbrot Maps. He's looking for feedback. Try it out!
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
11.3.20
Coronavirus: Why You Must Act Now
Labels: Academia, Covid-19, Politics, Scotland
4.3.20
Try out the new Mandelbrot Maps
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
A Nearly Carbon-Neutral conference model
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.
This might be an interesting model for SIGPLAN/ACM to explore. Although the white paper suggests it as a replacement for conferences in a physical location, we could also try it out as a supplement to such a conference.
Labels: Academia, Climate Change, Politics
30.1.20
A Profound Pun
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
10.12.19
Programming Languages for Trustworthy Systems
The University of Edinburgh seeks to appoint a Lecturer/Senior Lecturer/Reader in Programming Languages for Trustworthy Systems. An ideal candidate will be able to contribute and complement the expertise of the Programming Languages & Foundations Group which is part of the Laboratory for Foundations of Computer Science (LFCS).
The successful candidate will have a PhD, an established research agenda and the enthusiasm and ability to undertake original research, to lead a research group, and to engage with teaching and academic supervision, with expertise in at least one of the following:
- 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
We are seeking current and future leaders in the field.
Applications from individuals from underrepresented groups in Computer Science are encouraged.
Appointment will be full-time and open-ended.
The post is situated in the Laboratory for Foundations of Computer Science, the Institute in which the School's expertise in functional programming, logic and semantics, and theoretical computer science is concentrated. Collaboration relating to PL across the School is encouraged and supported by the School's Programming Languages Research Programme, to which the successful applicant will be encouraged to contribute. Applicants whose PL-related research aligns well with particular strengths of the School, such as machine learning, AI, robotics, compilers, systems, and security, are encouraged to apply and highlight these areas of alignment.
All applications must contain the following supporting documents:
• Teaching statement outlining teaching philosophy, interests and plans
• Research statement outlining the candidate’s research vision and future plans
• Full CV (resume) and publication list
The University job posting and submission site, including detailed application instructions, is at this link:
Applications close at 5pm GMT on January 31, 2020. This deadline is firm, so applicants are exhorted to begin their applications in advance.
Shortlisting for this post is due early February with interview dates for this post expected to fall in early April 2020. Feedback will only be provided to interviewed candidates. References will be sought for all shortlisted candidates. Please indicate on your application form if you are happy for your referees to be contacted.
Informal enquiries may be addressed to Prof Philip Wadler (wadler@inf.ed.ac.uk).
Lecturer Grade: UE08 (£41,526 - £49,553)
Senior Lecturer or Reader Grade: UE09 (£52,559 - £59,135)
The School is advertising a number of positions, including this one, as described here:
About the Laboratory for Foundations of Computer Science
As one of the largest Institutes in the School of Informatics, and one of the largest theory research groups in the world, the Laboratory for Foundations of Computer Science combines expertise in all aspects of theoretical computer science, including algorithms and complexity, cryptography, database theory, logic and semantics, and quantum computing. The Programming Languages and Foundations group includes over 25 students, researchers and academic staff, working on functional programming, types, verification, semantics, software engineering, language-based security and new programming models. Past contributions to programming languages research originating at LFCS include Standard ML, the Edinburgh Logical Framework, models of concurrency such as the pi-calculus, and foundational semantic models of effects in programming languages, based on monads and more recently algebraic effects and handlers.
About the School of Informatics and University of Edinburgh
The School of Informatics at the University of Edinburgh is one of the largest in Europe, with more than 120 academic staff and a total of over 500 post-doctoral researchers, research students and support staff. Informatics at Edinburgh rated highest on Research Power in the most recent Research Excellence Framework. The School has strong links with industry, with dedicated business incubator space and well-established enterprise and business development programmes. The School of Informatics has recently established the Bayes Centre for Data Technology, which provide a locus for fruitful multi-disciplinary work, including a range of companies collocated in it. The School holds a Silver Athena SWAN award in recognition of our commitment to advance the representation of women in science, mathematics, engineering and technology. We are also Stonewall Scotland Diversity Champions actively promoting LGBT equality.
Labels: Academia, Computing, Edinburgh, Formal Methods, Functional Programming, Programming Languages
9.12.19
Election Special: Antisemitism
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
Election Special: NHS
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
17.10.19
Caitlin Kirby defends her dissertation wearing a skirt made of rejection letters
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
16.10.19
How Amazon Web Services Uses Formal Methods
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
14.10.19
The Next 7000 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
13.10.19
Toki Pona
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.
1.10.19
Instead of flight shaming, let's be thoughtful and selective about all travel
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
7.8.19
IOHK is hiring!
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
22.5.19
Please vote!
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
PLFA in Padova
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
28.3.19
Pinker's Thirteen Rules for Better Writing
Steven Pinker tweets thirteen rules for better writing. Spotted via Boing Boing.
- Reverse-engineer what you read. If it feels like good writing, what makes it good? If it’s awful, why?
- Prose is a window onto the world. Let your readers see what you are seeing by using visual, concrete language.
- 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.”
- Let verbs be verbs. “Appear,” not “make an appearance.”
- 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.
- Omit needless words (Will Strunk was right about this).
- Avoid clichés like the plague (thanks, William Safire).
- Old information at the beginning of the sentence, new information at the end.
- Save the heaviest for last: a complex phrase should go at the end of the sentence.
- 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.”
- Revise several times with the single goal of improving the prose.
- Read it aloud.
- Find the best word, which is not always the fanciest word. Consult a dictionary with usage notes, and a thesaurus.
24.3.19
Two weeks of teaching in Ethiopia
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.
All the students in traditional dress for graduation. They wear it well!
Labels: Blockchain, Haskell, IOHK
Root causes
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
7.12.18
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.
Labels: Blockchain, Edinburgh, Haskell
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.
Labels: Brexit, EU, Europe, Politics, UK
