the problem I had with Dafny was the automated prover abruptly driving off a complexity cliff. the strategy is to build "tactic" functions that don't run at run

the problem I had with Dafny was the automated prover abruptly driving off a complexity cliff. the strategy is to build "tactic" functions that don't run at runtime but discharge a proof obligation at compile time. I'd be ecstatic if LLMs could write those tactic functions. Unfortunately, they're not great at the reasoning and preciseness required (plus their training data isn't exactly overflowing with Dafny proofs.)