[Peter_Sewell]

There's work along these lines (substantially predating Sail, but one could in principle do much the same starting from Sail specs) by Dias and Ramsey, e.g. the POPL 2010 and 2011 papers at https://www.cs.tufts.edu/~nr/

[ampdepolymerase]

This is how Go's assembler works.