Comment by nextaccountic

Types, preconditions and theorems are still a guardrail

Agents perform better when programming in Rust than <insert dynamic language here> (at least in my experience), exactly because types matter. Those theorem provers just have a poweful and pedantic type system that insists in being always correct, in detriment of everything else

LiquidHaskell (or flux or creusot in Rust) would be an improvement over Haskell or Rust too.

In either case (full blown theorem provers, or theorem provers laid on top of regular programming languages) the models would need to either focus in posttraining on coming up with good invariants to establish, or you need to prompt agents in a very specific way to get desired results (OP complains that sometimes Claude doesn't want to do this stuff, this happens when it's in out of distribution territory)