logoalt Hacker News

antonvsyesterday at 3:38 PM3 repliesview on HN

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.


Replies

jmalickitoday at 3:15 AM

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?

show 1 reply
drrotmosyesterday at 3:50 PM

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.

fzzzyyesterday at 4:07 PM

Luckily that's the compiler's job.

show 1 reply