Comment Comment by sealeck > I wrote a compiler that takes C and Rust code and compiles it to LeanWhat if there are bugs in this C,Rust->Lean compiler? Anthropic are able to sidestep this by reasoning at the RISC V level for which its easier to develop a correct semantics. parent sealeck 7 days ago
What if there are bugs in this C,Rust->Lean compiler? Anthropic are able to sidestep this by reasoning at the RISC V level for which its easier to develop a correct semantics.