Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
lukerj00
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
7 ms
·
1.
▲
by
lukerj00
4mo ago
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 diffe
2.
▲
by
lukerj00
4mo ago
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