This is really cool! However, I was somewhat disappointed that it only models a linearizable memory (each low-level operation atomically acts on the same global state). It would be great to teach people that they can't actually think about memory this way, since various reorderings are possible. The UI design gets a lot trickier, but this could become a great way to teach people how to deal with things like atomic instructions, memory fences, and the differences between the x86 and ARM memory models.