Abstract Machine Models (2022)

Fun read. My take on the "special something" that causes people to care about implementation is that you want to specifically control parts of a computer. Yes, this is typically for run-time performance; but crucially it is because you want to specifically reason about what the computer will be doing to implement your program. And the more that your computer is capable of doing, the more you are likely to care about different aspects of how it executes.

I'd hazard this goes both ways, too. That is, it is not just in terms of how much the computer is capable of doing, but what the real world systems being modeled can do. For a fun example, you can make a sorting network that can sort integers on a computer rapidly, but that doesn't necessarily help you sort a physical quantity of anything. Is akin to making a computer that can win a game of chess, but only if the human moves the pieces for it.

All too often, people present programs as if they are truths independent of either model or computer. Which is doubly wrong as they are constrained by the model of the language they are implemented in, as well as being dependent on the model of whatever problem they are describing.

The need for better parallel machine AMMs is particularly noticeable when writing lock-free data-structures. I often learn more by just looking at the disassembly of the compiler output on diverse architectures than I do from reading the manuals describing what their various memory-barrier operations do.

I think a formalism for AMMs might go a long way toward making formal software development more straightforward. All the formalisms I am aware of pair some logic with some programming language, or worse a logic with an abstract model of a language, but implicitly or explicitly portions of architecture get dragged into the formalism as well, e.g. resulting in seL4 having differing levels of proofs for various architectures (arm, amd64, risc-v).

If instead we pair a logic with a parameterized (by cache coherency semantics, hardware protection and isolation levels, register layout, etc.) abstract machine model then it could presumably apply over multiple architectures and languages with derived specializations for each language.

I didn't like the article.

I feel like some authors would really benefit from writing a first draft and then condensing it down to 1/n. In this case, like 1/10.

The author has an interesting and explicit model as a table for how to classify some languages. Everything else is either fluff or should be a separate article. For example, you either assume we're talking about moder languages, or your model needs to be way broader and more theoretical. Tangents about days when langauges were tied (at least way more than today) to hardware were unnecessary. That also goes for the biased way the author talks about their favorite languages.

It's also rife with things that, quite frankly speaking - I don't know what the hell they're talking about. It's almost like satire about how Haskellers are so clueless that they never think about run-time considerations. Or meandering thoughts on language theory (gotta drop in references to random wiki articles somehow I guess) about how it shapes our thoughts which don't amount to much because they say nothing interesting because they keep it too vague where the real answer is it depends. Or the loaded statements the author makes about Rust (in an honestly confusing way by framing it through the paretto front). Rust does not have the same guarantees as something with GC like Java. Even if you disagree with me on that, we should at least agree that this isn't as settled as the author makes it out to be.