3 ms·
The weakness goes beyond lifetimes. In Rust programs with non-trivial type schemas, it can really struggle to get the types right. You see something similar wit
by antonvs 10mo ago
The weakness goes beyond lifetimes. In Rust programs with non-trivial type schemas, it can really struggle to get the types right. You see something similar with Haskell. Basically, proving non-trivial correctness properties globally is more difficult than just making a program work.
- drrotmos 10mo agoTrue. I do however like the process of working with an AI more in a language like Rust. It's a lot less prone to use ugly hacks to make something that compiles but fail spectacularly at runtime - usually because it can't get the ugly hacks to compile :D Makes it easier to intercede to steer the AI in the right direction.
- fzzzy 10mo agoLuckily that's the compiler's job.
- antonvs 10mo agoYes, I was referring to writing the proofs, which is very much the human or LLM's job.
- jmalicki 10mo agoHow 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?
- antonvs 10mo agoYes, because those other languages all have much weaker type systems.
- jmalicki 10mo agoDo 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!