| ▲ | malisper 3 hours ago | ||||||||||||||||
For those skeptical, I've had decent success using formal verification for my Rust rewrite of Postgres. I wrote a compiler that can translate both Rust and C code into Lean. Once those two functions are in Lean, I have an LLM write a Lean proof that they behave identically. So far, I've proven that about 12% of the code behaves the same when executed single-threaded. That works out to roughly 70k lines of C code. This has found very minor differences in behavior, such as how floating-point operations across platforms can produce different results. I'm working on figuring out how to scale this up, but I don't see any fundamental limitation that would prevent this from scaling up further. | |||||||||||||||||
| ▲ | remywang 19 minutes ago | parent | next [-] | ||||||||||||||||
> I wrote a compiler that can translate both Rust and C code into Lean How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like a Herculean efforts | |||||||||||||||||
| ▲ | krukah 13 minutes ago | parent | prev | next [-] | ||||||||||||||||
Does your bilingual [Rust|C] -> Lean compiler fork rustc or clang, or other? 12% is promisingly high. I'm still hoping for a world where you can prove critical behavior w static analysis cheaply and practically. The overlap of LLMs and PLT feel under-explored to me pgrust is incredible btw | |||||||||||||||||
| ▲ | est31 2 hours ago | parent | prev [-] | ||||||||||||||||
Which models do you see to be productive for the task of writing lean? Big fan of pgrust. | |||||||||||||||||
| |||||||||||||||||