I don't see how you could generate a compiler backend from this -- the spec/pseudocode give you the "this instruction has these effects and side effects" mapping, but you can't easily reverse that to get the "if I want this effect then I need this instruction sequence" mapping which a compiler backend uses. Am I missing something?

As a gross simplification, a compiler is just a very complex pattern-matcher: it turns sequences of characters in source code into a series of machine instructions by matching the operations they perform. This spec gives part of that mapping, but it's probably quite sufficient: think about how a human can write Asm after reading the docs, and the algorithm (s)he uses to do that.

To give a concrete example, suppose you want to compile "c = a + b;". You would realise this is an addition operation, then look at the sizes of the variables and consider where they are/will be. You then search for instructions in the instruction set which can perform addition. Maybe the source operands are in memory and the only addition instructions operate on registers (like ARM) in which case you would then have to solve the sub-problem of getting them into a register, by searching for more instructions which do that; or perhaps (like x86) only one of the operands need be in a register, so you only need to solve that sub-problem once. After you've chosen an instruction, update the machine state and continue with the next operation. Etc. etc. A compiler uses a similar algorithm, and could be driven by this spec. It's not in a good form for efficient compilation (e.g. indexing by operation(s) performed would be far better), but it contains the necessary mapping.

Of course there are plenty of subtle details in this whole process, but it is very possible to do this type of "table-driven meta-compilation". At least for Asm, there are a few table-driven (dis)assemblers which operate on a very similar principle.

If anything, a "table-driven decompiler" using this spec might be a bit easier, since that is directly mapping machine instructions into their higher-level operations.

My point is that the spec does not give the behaviour-to-machine-instruction mapping, only the other way round, and reversing the mapping is non-trivial.

Table driven assemblers and disassemblers would be straightforward to produce from this spec, yes, because those just need to care about the instruction patterns and the mnemonics. A compiler backend needs to care about the semantics of the instructions, which are in the pseudocode, and thus harder to automatically reason about. (For instance lots of the instructions include an add somewhere, but how do you find the one that is just a plain add rather than saturating or simd or also setting the condition flags?) Writing something smart enough would I think be vastly more work than just doing a compiler backend by hand, and likely produce worse code anyway. (A sibling comment suggests it would be phd-thesis level work and I think I'd agree with that.)

I'm reasonably sure you can reverse it to get that, though I don't know what techniques would be used. "Easily" is another matter, though a good enough programming language would let you "prove" that you have a correct reverse mapping, for some definition of prove.

I agree - that should definitely be possible. Not necessarily easy though - but if anybody is looking for a PhD topic or, better yet, a whole research group looking for a challenge, you have all the bits you need to make it happen.