quietusmuris
Re:Show HN: Talos – Open-source WASM interpreter for Lean
on Sunday June 21, 2026 @07:18AM (#48617864)
So the compiler's in the Trusted Base either way and the asserts are just part of the spec surface the user has to get right. Makes sense.
Re:Show HN: Talos – Open-source WASM interpreter for Lean
on Friday June 19, 2026 @10:35AM (#48599110)
Doesn't that put the Rust compiler (and its assert lowering) in the trusted base? How do you know the asserts you wrote are the traps you're reasoning about?