4 ms·
> We thought about this and decided to just go all out and write a hypervisor which emulates a deterministic computer. Huh. Yes, that would work. It's in the c
by JonChesterfield 3y ago
> We thought about this and decided to just go all out and write a hypervisor which emulates a deterministic computer.
Huh. Yes, that would work. It's in the category of obvious in hindsight. That is a very convincing sales pitch.
- Smaug123 3y agoAlong similar lines, Mario Carneiro wrote a formalisation of a subset of x86 in MetaMath Zero (https://github.com/digama0/mm0/blob/master/examples/x86.mm0 https://github.com/digama0/mm0/blob/master/examples/x86.mm0) with the ultimate goal of proving that the MetaMath Zero verifier itself is sound. https://arxiv.org/pdf/1910.10703.pdf https://arxiv.org/pdf/1910.10703.pdf (And of course Permutation City is a fiction book all about emulating computers with sound properties!)