Wadler's Blog

 

Labels: Politics, US

 

Labels: Developers, Functional Programming, Programming Languages

From my colleague, John Longley, a treat. 

‘Informatics Lecturer Song’ 

I am the very model of an Informatics lecturer,
For educating students you will never find a betterer.
I teach them asymptotics with a rigour that’s impeccable,
I’ll show them how to make their proofs mechanically checkable.
On parsing algorithms I can hold it with the best of them,
With LL(1) and CYK and Earley and the rest of them.
I’ll teach them all the levels of the Chomsky hierarchy…
With a nod towards that Natural Language Processing malarkey.

I’ll summarize the history of the concept of a function,
And I’ll tell them why their Haskell code is ‘really an adjunction’.
In matters mathematical and logical, etcetera,
I am the very model of an Informatics lecturer.

For matters of foundations I’m a genuine fanaticker:
I know by heart the axioms of Principia Mathematica,
I’m quite au fait with Carnap and with Wittgenstein’s Tractatus,
And I’ll dazzle you with Curry, Church and Turing combinators.
I’ll present a proof by Gödel with an algebraic seasoning,
I’ll instantly detect a step of non-constructive reasoning.
I’ll tell if you’re a formalist or logicist or Platonist…
For I’ll classify your topos by the kinds of objects that exist.

I’ll scale the heights of cardinals from Mahlo to extendible,
I’ll find your favourite ordinals and stick them in an n-tuple.
In matters philosophical, conceptual, etcetera,
I am the very essence of an Informatics lecturer.

And right now I’m getting started on my personal computer,
I’ve discovered how to get it talking to the Wifi router.
In Internet and World Wide Web I’ve sometimes had my finger dipped,
And once I wrote a line of code in HTML/Javascript.
[Sigh.] I know I have a way to go to catch up with my students,
But I try to face each lecture with a dash of common prudence.
When it comes to modern tech: if there’s a way to get it wrong, I do!
But that seems to be forgiven if I ply them with a song or two.

So… although my present IT skills are rather rudimentary,
And my knowledge of computing stops around the nineteenth century,
Still, with help from all my colleagues and my audience, etcetera…
I’ll be the very model of an Informatics lecturer.

Labels: Computing, Edinburgh, Programming Languages, Theatre, University

How is this not illegal??? Cards Against Humanity is PAYING people who didn't vote in 2020 to apologize, make a voting plan, and post #DonaldTrumpIsAHumanToilet—up to $100 for blue-leaning people in swing states. I helped by getting a 2024 Election Pack: checkout.giveashit.lol. Spotted via BoingBoing. More info at The Register. (Only American citizens and residents can participate. If, like me, you are an American citizen but non-resident, you will need a VPN.)

Labels: Politics, US

 

Happy Election Day!

The above shows an average of five recent polls for my constituency, Edinburgh North and Leith, and comes courtesy of Stop the Tories. Clearly, the Tories have no chance, but I will still be voting tactically. I am a member of the Greens. But if everyone who intends to vote Green instead votes SNP, the SNP will beat Labour (rather than the other way around). While the SNP has made some awful missteps of late, they are the best hope to push Labour toward the more progressive policies from which Starmer has dragged them away. My tactical vote goes to the SNP.

Labels: Politics, Scotland, UK

I'm looking forward to speaking in Lisbon. 

On June 4, Professor Philip Wadler will give an INESC-ID Distinguished Lecture organized in the scope of the BIG ERA Chair Project, titled “(Programming Languages) in Agda = Programming (Languages in Agda)”.

Registration: here (free but mandatory)
Date: June 4, 2024
Time: 15h00-16h15
Where: Anfiteatro Abreu Faro – Complexo Interdisciplinar, Instituto Superior Técnico (Alameda) 

Abstract: The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. Proof by induction is just programming by recursion.  Finding a proof becomes as fun as hacking a program. Dependently-typed programming languages, such as Agda, exploit this pun. This talk introduces *Programming Language Foundations in Agda*, a textbook that doubles as an executable Agda script—and also explains the role Agda plays in IOG’s Cardano cryptocurrency.

Labels: Agda, Programming Languages

I am delighted to have made this list. Lesley Lamport and John Reynolds also appear on it, but at positions lower than mine, and Tony Hoare and Robin Milner don't appear at all---so perhaps their methodology needs work.

Congratulations on being named an inaugural Highly Ranked Scholar by ScholarGPS

Dear Dr. Wadler,

ScholarGPS celebrates Highly Ranked Scholars™ for their exceptional performance in various Fields, Disciplines, and Specialties. Your prolific publication record, the high impact of your work, and the outstanding quality of your scholarly contributions have placed you in the top 0.05% of all scholars worldwide.


Listed below is a summary of the areas (and your ranking in those areas) in which you have been awarded Highly Ranked Scholar status based on your accomplishments over the totality of your career (lifetime) and over the prior five years:

Highly Ranked Scholar - Lifetime
#9,339	Overall (All Fields)
#1,299	Engineering and Computer Science
#265	Computer Science
#2	Programming language

Please consider sharing your recognition as an inaugural ScholarGPS Highly Ranked Scholar with your employer, colleagues, and friends.

ScholarGPS also includes quantitative rankings for research institutions, universities, and academic programs across all areas of scholarly endeavor. ScholarGPS provides rankings overall (in all Fields), in 14 broad Fields (such as Medicine, Engineering, or Humanities), in 177 Disciplines (such as Surgery, Computer Science, or History), and in over 350,000 Specialties (such as Cancer, Artificial Intelligence, or Ethics).

We are pleased to currently offer you free access to each of the following:

• All Scholar Profiles and Scholar Rankings based on either lifetime achievements or on accomplishments over the past five years.
• Lists of Highly Ranked Scholars categorized by Field, Discipline, and Specialty. Highly Ranked Scholars™ are the most productive (number of publications) authors whose works are of profound impact (citations) and of utmost quality (h-index). Their scholarly contributions position them within the top 0.05% of all scholars worldwide.
• Institutional Rankings and program rankings that are based on the achievements of institutional scholars over their lifetime and over the past five years.
• Profiles for Fields, Disciplines and Specialities, including a summary of activities, associated ranked institutions, Highly Ranked Scholars, and highly cited publications.
• Top Scholars by Institution or Top Scholars by Expertise or Top Scholars by Country by ranking order across All Fields, Field, Discipline, or Specialty. Top scholars are those authors whose scholarly contributions position them within the top 0.5% of all scholars worldwide.
• Institutional profiles including a summary of activities, associated program rankings, Highly Ranked Scholars, Top Scholars, and highly cited papers as well as publication and citation histories. View both Highly Ranked Scholars and Top Scholars within each institution categorized by Field, Discipline, and Specialty.
• A user-friendly publication search capability and corresponding citation index.

Sincerely,
The ScholarGPS Team

Labels: Programming Languages

I'll be appearing at the Fringe in the Cabaret of Dangerous Ideas, 12.20-13.20 Monday 5 August and 12.20-13.20 Saturday 17 August, at Stand 5. The 5 August show is joint with Matthew Knight of the National Museums of Scotland, the 17 August show is all mine. Both shows are hosted by comedian Susan Morrison.

You can book either via the Fringe or via the Stand. If one is sold out, try the other.

Here's the brief summary:

Chatbots like ChatGPT and Google's Gemini dominate the news. But the answers they give are, literally, bullshit. Historically, artificial intelligence has two strands. One is machine learning, which powers ChatGPT and art-bots like Midjourney, and which threatens to steal the work of writers and artists and put some of us out of work. The other is the 2,000-year-old discipline of logic. Professor Philip Wadler (The University of Edinburgh) takes you on a tour of the risks and promises of these two strands, and explores how they may work better together.

I'm looking forward to the audience interaction. Everyone should laugh and learn something. Do come!

I'm looking forward to Lambda Days 2024 and catching up with friends in Krakow.

Labels: Functional Programming

 

A short comic by Mike Dawson. Stick to the end for a valid point.

Labels: Comics, Communication, Politics, Writing