3 ms·
Correctness is typically checked long before code generation happens. This does mean the code generation backend must be trusted, whether the target be x86 or w
by ehsanu1 9y ago
Correctness is typically checked long before code generation happens. This does mean the code generation backend must be trusted, whether the target be x86 or wasm. Just as you have to trust CPUs to not expose processes' memory to each other (oops).
- eastWestMath 9y agoTyped assembly is a thing - it’s mainly to ensure the compiler itself is correct, but it does give stronger guarantees. I think Frank Pfenning at CMU has written a language that’s dependently typed all the way down - so it’s IR and assembly are both dependently typed.