What was the best CS paper you read in 2022?

amw-zero

edited 5 hours ago

| link

Are you asking for ones published in 2022? The best one that I read in 2022 was published in 2017. It’s Refinement through Restraint: Bringing Down the Cost of Verification. It’s about the Cogent language, which is used to write formally verified filesystems. The way it does this is amazing.

It starts with the paradigm of certifying compilation, which is where the compiler outputs proof of its correctness in addition to the actual compiled target code. The theory behind compiler correctness is super interesting (refinement and simulation), which this paper gives a great overview of. But on top of that, in order to produce this certificate proof, the compiler compiles multiple different artifacts on each run, including an embedding of the source code in the Isabelle proof assistant. It’s just a really cool, mind-expanding idea.

Now, most people don’t formally verify their entire application. But this paper inspired me to work on my own language project that takes this high level idea, but makes a couple of tweaks. First, I drop the formality requirement and instead produce a test for correctness instead of a proof. Second, the compiler isn’t intended to produce machine code, but to produce an entire application from a high-level specification. Like, I’m using it to generate web applications, not assembly code.

This is a really interesting workflow where you get tests generated for you for free, and instead of writing tons of unit tests you can just run this one test to see if your compiled application is correct based on the specification. No free lunch of course - the generated test is a large integration test, and you end up trading of the time it takes to write the test for test execution time. But, scaling up test runners is easy. Scaling up programmers is more difficult, in my opinion.

So yea. Pretty niche stuff, but this was the most influential paper I read last year.