| ▲ | remywang an hour ago | |
> 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 Herculean efforts | ||
| ▲ | malisper 4 minutes ago | parent [-] | |
> How do you verify this compiler is correct? I haven't yet. My main goal has been to find as many bugs as possible. While bugs could still slip through because my compiler is incorrect, I'm still finding a good number, so I think it's worth it. | ||