[antonvs]

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]

True. 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.

[jmalicki]

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?

[antonvs]

Yes, because those other languages all have much weaker type systems.

[jmalicki]

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!

[fzzzy]

Luckily that's the compiler's job.

[antonvs]

Yes, I was referring to writing the proofs, which is very much the human or LLM's job.