The language of code: type checking for Wyvern
Even for the non-technical, many of the characteristics of programming work are as most of us imagine them: precise, painstaking, and utterly dependent on accuracy. One of the ways programmers ensure this accuracy is through ‘type checkers’—tools that check for errors in code in the same way that we might use a spellcheck in a Microsoft Word document. How, though, do we make sure code is consistent if type checkers aren’t reliable? School of Engineering and Computer Science PhD candidate Julian Mackay’s research examines exactly this issue.
“Sometimes algorithms capable of reliably type checking all possible programs just don’t exist. It’s referred to in the field as ‘undecidability’”, Julian explains. “Type checking of some of the key programming languages is currently undecidable.” The result? Programs in widely used languages such as Java or Scala can cause type checkers to crash during compilation.
Julian and his supervisory team developed a solution to this problem for the Wyvern programming language. With this extension, Wyvern is completely ‘decidable’ and programs written in the Wyvern language are all able to be type checked. The language builds on the keen interest Julian has developed in programming languages, and particularly in their mathematical foundations. “Victoria University of Wellington’s active programming languages research group has helped drive my interest in software and how it is designed,” he explains.
Julian began his studies with a Bachelor of Science in Mathematics and Computer Science, and completed a Master of Science in Computer Science before embarking on his PhD. “This project was the central aim of my PhD thesis. It’s something that I’ve worked on in conjunction with my VUW supervisors, A/Prof Alex Potanin and A/Prof Lindsay Groves, as well as Professor Jonathan Aldrich at Carnegie Mellon University in Pittsburgh, Pennsylvania.”
As with any research, it has been a long road to see their design for Wyvern come to fruition, and there have been many roadblocks along the way. Julian explains that there have been several iterations of the team’s design, each building on the last, and incorporating feedback from researchers in the wider programming languages community.
“Not only is it possible to type check any Wyvern program,” Julian notes, “but it’s closely related to Scala (a programming language that is relatively widely used) and able to express many of the patterns expressed in Scala.”
“Scala 3, a new and highly anticipated version of Scala, is due to be released at the beginning of next year,” Julian adds. “We hope that our work might inform the design of Scala 3, and help eliminate unexpected errors from Scala users’ code. It’s a language that sees a lot of industry usage, so ensuring tools such as type checkers are reliable is important.”
The next step for Julian is presenting his Wyvern research at the prestigious Principles of Programming Languages (POPL) conference in New Orleans in 2020. This places Julian amongst only a handful of New Zealanders to ever present at the conference. “Over the last few decades POPL has published some of the most significant papers in the area of programming languages,” he notes.