PLSE Blog

Before I ever started my PhD, I could have recited to you the Curry-Howard Isomorphism: proofs are programs, and programs are proofs. But it was only when I started working on proof compilation in the interactive theorem prover Rocq (formerly known as Coq) that I feel that I truly understood it – along with why it works, why theorem provers work, and all sorts of cool tricks and connections you can use.

If you saw my last blog post, you know that I work on design tools for knitting unusual things. Today I’m introducing my new project, which is a design tool to support knitting things in unusual ways. I’m also introducing my new amazing collaborator, Marlena!

Once UW kicks off the school year at the end of this month, I’ll officially be a second-year PhD student It’s a scary, yet exciting, thought! There will be loads of new incoming students, interesting research, and many surprises in store! This is also the perfect time to think critically about my goals in the PhD. One of them is building a larger theme for my research. I’m not committing to a thesis topic here. Rather, I’m searching for a concise, ideally pithy, way to describe my research. This blog post is a trial run for one theme: Real Analysis through the lens of Programming Languages.

This summer, I’ve been interning at Sandia National Labs, working on extending CompCert for concurrent programs. We represent program states as a list of threads t :: ts and a memory state m. Much of my work relates to trying to formalize safety properties of the memory state as the program steps. This is my first time using Rocq outside of CSE 505, so I thought it would be interesting to write up some reflections on the experience.

Over the past year (and … mostly right before this post was published), I’ve been working with our wonderful website chair Yihong to make small web accessibility improvements to the PLSE website. I wanted to spend a bit of time writing up what we’ve done for a couple of reasons, which will coincidentally also sketch out the structure of this post:

When discussing programming languages, there are often two axes that we care about: syntax and semantics. In my first post about Verilog, I discussed the interesting points of Verilog's syntax. This post will discuss Verilog semantics. Specifically, whereas the first post covered the basics of structural Verilog, this post will introduce the basics of behavioral Verilog.

Getting hardware right is crucial – without correct hardware, there’s no way to guarantee that software will work as intended. To raise the stakes even higher, hardware designers really only have one shot to get it right – once the hardware’s made, you can’t really patch it! To address this importance, there are many tools which use formal methods to give strong guarantees that hardware is correct. In practice, this often entails writing equivalence proofs showing that hardware behaves the same as some high-level model. In this post, we’ll take a look at the challenges I ran into while making Gator, a project I worked on which explored how to make these proofs easier!

In 1931, Kurt Godel stunned the world of mathematics when he published his “Incompleteness Theorem.” To summarize, the theorem stated that, no matter what set of rules we believe to be true about our world, there will always be statements that are… unprovable. This infuriated various mathematicians, who had believed that mathematics would be the key to proving everything! Now, I am not a mathematician, and this blog post is not a discussion of logic. However, this research (which I promise we will discuss momentarily) is often plagued by a strong desire for absolute correctness and proof, much like the mathematicians of the past. This ailment is in direct opposition with the only true rule known about the world of software testing, which is: Software testing is very hard.

Every programmer loves writing tests, but tests can’t say much about the correctness of your program. Wait a minute, what? You mean I’ve been writing tests all this time for absolutely nothing? I’ve been lied to in my undergrad software engineering course? Unfortunately, it seems like we’ve known this fact since at least 1969. A transcript from a conference on software engineering techniques sponsored by the NATO science committee contains the following quote by Edsger W. Dijkstra:

The past few weeks, I’ve been learning more about a few different kinds of weaving. One form of weaving is card weaving (also called tablet weaving), where the loom is instead replaced by square pieces of cardboard with holes punched in each corner. You may be wondering: how does a bunch of pieces of cardboard with holes weave cloth? I wondered the same thing myself! It seemed bonkers to think that you could do something with a bunch of cards that produced anything like fabric.