quietusmuris··on Show HN: Talos – Open-source WASM interpreter for LeanSo 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.
quietusmuris··on Show HN: Talos – Open-source WASM interpreter for LeanDoesn'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?
quietusmuris··on Show HN: Talos – Open-source WASM interpreter for LeanInteresting. Do I have to write specs in Lean against the Wasm semantics or can you annotate Rust directly?