My First Type Theory

Who knew? Add eyeballs and rhymes, and type theory becomes cute! An introductory video by Arved Friedemann.

Hokusai's "The Great Wave" recreated in Lego

 

Brilliant! Spotted via Boing-Boing.

Lego Certified Professional Jumpei Mitsui brought Hokusai's iconic ukiyo-e woodblock print "The Great Wave off Kanagawa" (c. 1829-1833) into the Lego realm. Marvel at this incredible work in Osaka's Hankyu Brick Museum.

A Year of Radical No's

Sue Fletcher-Watson describes her plan for A Year of Radical No's and follows up with Nine Months of Saying No – an update. Thanks to Vashti Galpin for the pointer!

So my main fear was that this Strategic Leadership Course would try to feed me time management tips, taking up 6 precious days of my time, when what I need is just LESS WORK. Thank the lord, far from it. ... One session left a particularly strong impression on me.  We spent some focused time considering the work-life balance challenges of another person on the course, culminating in offering them some advice. My advice? Say No, for a whole year, to everything new. Conferences, training, collaborations, journal reviews, student supervisions, the whole lot. Their response? Laughter.  None of us could imagine doing such a thing.

"This must be your first"

Zeynip Tufekci, writing in The Atlantic, explains why Trump's ludicrous attempt at a coup cannot be laughed away.

The next attempt to steal an election may involve a closer election and smarter lawsuits. Imagine the same playbook executed with better decorum, a president exerting pressure that is less crass and issuing tweets that are more polite. If most Republican officials are failing to police this ham-handed attempt at a power grab, how many would resist a smoother, less grossly embarrassing effort?

(Image from Tom the Dancing Bug.)

A Tale of Two Pandemics

A Tale of Two Pandemics: A graphic summary explaining how and why communities of colour suffer more from Covid. Spotted via BoingBoing.

Recursive image rotation

 

A striking visual example of recursion!

English universities are in peril because of 10 years of calamitous reform

 

Stefan Collini writes in the Guardian.

Then there is the rather less obvious contradiction between consumerism and education. Our higher education system is at present structurally consumerist. Even now, it is not widely understood how revolutionary were the changes introduced in 2010-12 by the coalition government in England and Wales (Scotland wisely followed another course). It wasn’t simply a “rise in fees”. It was a redefinition of universities in terms of a market model. The Office for Students is explicitly a “consumer watchdog”. Consumers are defined by their wants; in exchange for payment they are “entitled” to get what they ask for. ...

Universities are, by a long way, the main centres of research and scholarship in our societies; they curate the greater part of our intellectual and cultural inheritance; they provide by far the best source of disinterested expertise; they select and prepare those who will be the scholars and scientists of the future, and so on. Countries all over the world have found that you cannot fulfil these functions by distributing students and academics across all institutions either uniformly or randomly. Some element of selection and concentration is needed, and that brings with it some element of hierarchy, however unofficial. Explicit differentiation of function among higher education institutions might well be preferable to any pretence that they are all doing the same thing and doing it equally well.

Six questions that predict success

 Carol Dweck, a Stanford psychologist famous for her research on growth mindset, is coauthor of a new study.

To test the theory, the researchers asked student participants six questions and asked them to rate themselves on a 1 (never) to 5 (always) scale.

• When you are stuck on something, how often do you ask yourself, "What are things I can do to help myself?"
• Whenever you feel like you are not making progress, how often do you ask yourself, "Is there a better way of doing this?"
• Whenever you feel frustrated with something, how often do you ask yourself, "How can I do this better?"
• In moments when you feel challenged, how often do you ask yourself, "What are things I can do to make myself better at this?"
• When you are struggling with something, how often do you ask yourself, "What can I do to help myself?"
• Whenever something feels difficult, how often do you ask yourself, "What can I do to get better at this?"

What happened? Higher scores predicted higher grades.

And in subsequent studies, higher scores predicted greater success in a professional challenge and in a health and fitness goal.

Five stages of accepting constructive mathematics

 

From a psychological point of view, learning constructive mathematics is agonizing, for it requires one to first unlearn certain deeply ingrained intuitions and habits acquired during classical mathematical training. In her book On Death and Dying psychologist Elisabeth Kubler-Ross identified five stages through which people reach acceptance of life’s traumatizing events: denial, anger, bargaining, depression, and acceptance. We shall follow her path.

Five stages of accepting constructive mathematics is a nifty introduction to constructive mathematics by Andrej Bauer. Mentioned by Martin Escardo on the Agda mailing list. 

Positive Obsession and Furor Scribendi

 

I've just completed reading a trio of books by Octavia Butler: The Parable of the Sower, The Parable of the Talents, and Bloodchild and Other Stories. The latter contains two essays, Positive Obsession and Furor Scribendi, which I heartily recommend. Replace writer by researcher and everything remains true.

Persistence is essential to any writer--the persistence to finish your work, to keep writing in spite of rejection, to keep reading, studying, submitting work for sale. But stubbornness, the refusal to change unproductive behavior or to revise unsalable work can be lethal to your writing hopes.

Octavia Butler, "Furor Scribendi"

Don't Stop ICFP

The ICFP music video is out! Thank you to Youyou Cong and Jose Calderon for putting this together. They've done the community a great service.

Segregated by Design

Systematic racism stunts the opportunities available to blacks, but I've seen few clear explanations of it mechanisms. Segregated by Design lays bare these mechanisms as regards housing, explaining how federal, state, and local policies deliberately fostered segregation in contravention of the constitution. Lucid, to the point, and graphically inventive. Animated by Mark Lopez, based on The Color of Law by Richard Rothstein.

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.

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.

An Incredible Scientific Breakthrough Discovery to Beat Covid

I almost never see masks in Edinburgh, not even in stores or on busses. Brazil has serious problems, but no one in Rio de Janeiro goes outside without a mask. Courtesy of Tom the Dancing Bug.

Haskell Love

I am speaking at Haskell Love, 31 July--1 August 2020,  a virtual event.

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.

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.

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

Who is beating Covid 19?

Interesting data from EndCoronavirus.org.

PhD position in Certifying Compilation of Smart Contracts

Wouter Swierstra at Utrecht and my IOHK colleague Manuel Chakravarty are looking for someone to undertake a PhD to build a certifying compiler for our smart contract language, Plutus.

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.

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.

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.

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

The New New Yorker

Courtesy of Tom The Dancing Bug.

XKCD vs Coronavirus

Thank you, XKCD!

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.

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!

Coronavirus: Why You Must Act Now

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!

Try out the new Mandelbrot Maps

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]).

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.

A Profound Pun

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