Philip Wadler

Co-creator of Haskell, Professor of Theoretical Computer Science at University of Edinburgh

Philip Wadler likes to introduce theory into practice, and practice into theory. An example of theory into practice: GJ, the basis for Java with generics, derives from quantifiers in second-order logic. An example of practice into theory: Featherweight Java specifies the core of Java in less than one page of rules. He is a principal designer of the Haskell programming language, contributing to its two main innovations, type classes and monads. The YouTube video of his Strange Loop talk Propositions as Types has over 100,000 views.

Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK. He is a Fellow of the Royal Society, a Fellow of the Royal Society of Edinburgh, and an ACM Fellow. He is head of the steering committee for Proceedings of the ACM, past editor-in-chief of PACMPL and JFP, past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of over 70 with more than 25,000 citations to his work, according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O'Reilly, 2006), and Programming Language Foundations in Agda (2018). He has delivered invited talks in locations ranging from Aizu to Zurich.

Keynote: The Two Cultures of Artifical Intelligence

Everyone is talking about new advances in Artificial Intelligence (AI): texts written by ChatGPT, images drawn by Midjourney, and self-driving cars from Tesla.

When I was a sophmore I learned the fundamentals of my subject from John McCarthy, founder of AI and a pioneer of programming. In the early days, AI debated the merits of two complementary methods: logic vs heuristics. Typical of the first is proving properties of programs, which became my research interest. Typical of the second is machine learning, the foundation of ChatGPT, Midjourney, and self-driving.

This talk will contrast the two approaches, discussing the benefits and risks of each, and how the first may curb shortcomings of the second.

Artists and writers are worried that AI will put them out of a job. One of the next professions on the list is programmers. Already, ChatGPT and related systems can do a credible job of generating simple programs, such as code for web pages. However, also already, such systems have demonstrated that they routinely write code containing known security bugs.

One possible scenario is that heuristic techniques will prove as adequate as humans—and far cheaper—at simple tasks, putting writers, artists, and programmers out of work. Bereft of new data to learn from, the machine learning applications will then fall into stagnation. They will be fine at producing articles, art, and code close to what has been produced before, but unable to produce anything original. And by then there may no longer be writers, artists, or programmers to hire, as who would study for a profession where no one can find work because they’ve been displaced by machines?

A different scenario is to pass laws to ensure that writers and artists are fairly recompensed when AI generates artifacts based on their work. Regarding code, the logical techniques have shown they can vastly improve reliability. Synthesising logical and heuristic techniques may lead to code that is both cheaper and more reliable. Programmers would shift from writing code to writing logical specifications, with AI helping to generate code proved to meet those specifications.

REFERENCES
AI machines aren’t ‘hallucinating’, but their makers are. Naomi Klein. The Guardian, 8 May 2023.
https://www.theguardian.com/commentisfree/2023/may/08/ai-machines-hallucinating-naomi-klein
The problem with counterfeit people. Daniel Dennett. The Atlantic, 16 May 2023.
https://www.theatlantic.com/technology/archive/2023/05/problem-counterfeit-people/674075/
Will AI become the new McKinsey? Ted Chiang. The New Yorker (online), 4 May 2023.
https://www.newyorker.com/science/annals-of-artificial-intelligence/will-ai-become-the-new-mckinsey
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, July 2009, 52(7), pages 107–115. https://dl.acm.org/doi/pdf/10.1145/1538788.1538814
Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff. How Amazon Web Services Uses Formal Methods. Communications of the ACM, April 2015, 58(4), pages 66–73. https://dl.acm.org/doi/pdf/10.1145/2699417

←Back