PLSE Blog

Ten years since its inception, the Herbie project remains an active source of research and is a marquee project of PLSE. It directly spawned four publications: Herbie at PLDI 2015, Pareto-Herbie (Pherbie) at ARITH 2021, Rival at ARITH 2023, and Odyssey at UIST 2023, and influenced many more papers (see an incomplete list). However, as with any long-standing project, we must question the fundamental idea behind it to inspire new directions of work. Previously, we pitched Herbie as a numerical analyst’s companion, a tool that automatically improves the accuracy of floating-point expressions. Now, we reenvision Herbie as a numerical compiler for programmers, lowering real expressions to floating-point implementations that are optimized for a given platform.

In my own research on Computer Algebra Systems (CAS), I often work some pretty cool data structures 😎. In this post, I want to show off one that’s responsible for simplifying polynomials. But first, I have a little secret…In high-school, I thought polynomials were boring! The hours I spent finding roots dragged on and on. They didn’t make pretty graphs like the trig functions. It’s only at this point in my life that I more fully appreciate them.

Have you ever wondered why hardware security isn’t a solved problem? It’s been six years since Spectre and Meltdown sent tech companies scrambling to fix the vulnerabilities that hardware manufacturers created with their own optimizations. Everyone involved–chip manufacturers, big tech, the security community–seems to agree that hardware security bugs are Bad and To Be Avoided. So if everyone believes that these vulnerabilies shouldn’t happen, why do they keep happening?

Testing cannot ensure correctness, but verification can. The problem with a specify-and-verify approach is the first part: the specification. Programmers are often reluctant to write specifications because it seems like extra work, beyond writing the code.

One of the great joys of being a researcher is observing an interesting phenomenon and deciding that you want to understand it and recreate it. Then there’s the additional joy of being a knitting researcher, and having that phenomenon be a cool object you can also display in your house or wear!

Verilog is a language of fundamental importance. Yet, despite that fact, it is mostly ignored in the world of programming languages (PL) and compilers research. In this post, I present one very simple fact about Verilog programs: they represent pure expressions. In explaining this, I hope to make Verilog more approachable by a programming languages and compilers audience.

In the last post, we showed the connections between chase and techniques developed in databases literature and tree automata literature, and how these connections help us understand equality saturation (EqSat). In this blog post, we will focus on a specific problem EqSat faces: the termination problem¹, something my collaborators and I have been working on recently.

While “Goto Considered Harmful” (Dijkstra, 1968) is one of the most famous pieces of writing in Computer Science, its enduring relevance to programming languages is almost wholly unappreciated or — at best — misunderstood. Historically, supporters and detractors from the original letter have addressed themselves to the conclusion that use of the goto statement should be avoided. (Including Knuth [1]) Depressingly, it took over two decades [2] before anyone bothered to empirically test Dijkstra’s claim. To the best of my knowledge, no-one ever disputed, supported, or merely considered Dijkstra’s premises and form of argument.