Comment by antonvs
8 hours 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.
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.
Luckily that's the compiler's job.
Yes, I was referring to writing the proofs, which is very much the human or LLM's job.