Hacker News: lukerj00https://news.ycombinator.com/user?id=lukerj00Hacker News RSShttps://hnrss.org/hnrss v2.1.1Fri, 19 Jun 2026 22:17:44 +0000<![CDATA[New comment by lukerj00 in "Show HN: Talos – Open-source WASM interpreter for Lean"]]>More on this - LLVM-IR has no official formal semantics and it's riddled with UB. RISC-V has a formal model in Sail, but it's an ISA so you throw away the structured control flow and types which we want for proving.

Wasm has different levels we can validate against - starting with W3C test suite, then later full verification against the SpecTec-generated Lean semantics so that we can drop our interpreter from the trusted base.

]]>Fri, 19 Jun 2026 15:04:44 +0000https://news.ycombinator.com/item?id=48599448lukerj00https://news.ycombinator.com/item?id=48599448https://news.ycombinator.com/item?id=48599448<![CDATA[New comment by lukerj00 in "Show HN: Talos – Open-source WASM interpreter for Lean"]]>I’m on the Cajal team - not OP, but happy to answer questions.

The core bet is that Wasm is a good verification target (close to compiled artifacts, many languages target it), and Lean is the right place to do verification.

Super interested in hearing from people working with Lean, compilers or other Wasm verification frameworks (eg Iris-Wasm).

]]>Thu, 18 Jun 2026 14:50:57 +0000https://news.ycombinator.com/item?id=48586316lukerj00https://news.ycombinator.com/item?id=48586316https://news.ycombinator.com/item?id=48586316