Comment by jmalicki
1 month ago
How is this an issue specifically with Rust and Haskell? Do you find that LLMs have an easier time proving global correctness with C, Python, or Typescript?
1 month ago
How is this an issue specifically with Rust and Haskell? Do you find that LLMs have an easier time proving global correctness with C, Python, or Typescript?
Yes, because those other languages all have much weaker type systems.
Do you have examples of LLMs proving global correctness for say, C? Having worked on static analysis for both C and Rust, Rust is the easier problem because of the type system, but I am eager to be proven wrong!