[pron]

> Every time you compile a statically-typed programming language you are using formal verification

Yeah, this is not what we're talking about here. We're talking about proving properties with deep alternative quantifiers.

> That isn't just hard. Proving software correct in complete generally is impossible. There are all kinds of practical and fundamental constraints that leave it to be impossible. Verification is only useful when you are acting within the scope of a compressed specification of a system's behaviour.

Nobody said anything about complete generality. We're talking about the practice of applying formal methods. It's not writing in Rust, and it's not a general program verifier, but a practice that's applied in some parts of the industry and not others, as the article says.

Put another way, the question is: for those programs and those properties that humans are able to prove with proof assistants, how expensive is it for LLMs to do that work.