Comment by sealeck
9 hours ago
> I wrote a compiler that takes C and Rust code and compiles it to Lean
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.
My goal isn't to "prove" the software is correct. My goal is to find as many bugs as I can with the least effort. If I'm able to find all differences in behavior between pgrust and Postgres, sans bugs in the compiler, that's a real win for me
fwiw, I wouldn't say working at the assembly level solves the problem. You now need to make sure that your definition of the assembly behavior is correct