Wearing a khaki suit and a Panama hat, Philip Wadler meets his audience for the Distinguished Lecture (Programming Languages) in Agda = Programming (Languages in Agda), organized within the scope of the BIG ERA Chair Project. This time, we got the explorer’s look. For other attendees, the professor of Computer Science at the University of Edinburgh and a Fellow of the Royal Society has chosen the Superman costume.
Regardless of the cover, the expertise – spiced up with a touch of humour – is always assured. Wadler, a key developer of several programming languages, like Haskell and Java, is a notable figure in the field. “One of the most important personalities in the area”, Luís Caires, INESC-ID Information and Decision Support Systems and ERA Chair Holder, states while introducing the talk, which happened on June 4, at Instituto Superior Técnico (Alameda).
Wadler’s connection to Portugal comes through both the brain and the heart. “It’s a very strong place in programming languages!”, he notes. The emotional bond comes from his wife, a Brazilian native and a big fan of the country.
Author of several books on programming languages, the researcher and teacher has specialized in linear programming languages, “which is a tiny subfield of a subfield.” While talking about the subject, he often goes back to Ancient Greece and to the origins of the studies on logic, relating it to concepts like propositions as types and foundational logic ideas. “We’re working on programming languages that we’re designing now, but the designs are based on ideas and logic that go back to the turn of the 1900s or sometimes go back to Ancient Greece two thousand years ago.” Lewis Carroll, under his real name Charles Dodgson, also did some work on logic, Wadler exemplifies. “It is said that after Alice in Wonderland came out, the Queen of England said she wanted to see that author next book and it was on symbolic logic.”
Explaining the title of his talk, he explains Agda is one of a family of “what are called proof assistants”, that also go back in time, to the cryptography genius, Alan Turing. “Everybody is aware of this notion that programmes have bugs, right? You see this all the time: You’re using the web and all of a sudden, the website dies and puts up a little message saying ‘Please contact service or something’. So wouldn’t it be nice if you could demonstrate that would never happen?”, he questions. The sort of systems used by Amazon, for example, and that come in very handy in the cryptocurrency world and that is where his cooperation, as a consultant, with the platform Cardano comes from.
Writing proofs is not as simple as writing code. It requires highly trained individuals, who are not in abundance. “Artificial intelligence and machine learning classes and so on have around 400 students. My class has forty”, he compares.
Another sector that might benefit considerably from the use of proof assistants is Large Language Models. “What does a large language model do? It’s a neural network trained on a very large body of texts. What it does is given a group of words, what word should come next to sound good? So it’s just trained to sound good, to impress and therefore they have the tendency to confabulate”, Wadler notes. The integration of proof assistants on the programming of these models gives us the possibility to avoid these mistakes. But always with “people involved”, he stresses. “To check the specifications and come up with new ways of doing proofs and teach them to the machines.” Bulletproof logic.
Text by Sara Sá, Science Writer | Communications and Outreach Office, INESC-ID
Images | © 2024 INESC-ID