|
|
|
|
|
|
by win311fwg
33 days ago
|
|
|
Every time you compile a statically-typed programming language you are using formal verification, so we have all kinds of industrial scale examples. The reports suggest that outputting tokens for these languages is as easy for LLMs as Javascript. And actually, I would suggest that the reports indicate that LLMs find it easier to output tokens for those languages than Javascript. LLMs are laughably bad at writing Javascript. On the other hand we can watch humans struggle to do the same. How often have you heard things like "I won't use Rust because it is too hard to use"? I have never seen an LLM refuse to output Rust because it thought it was too hard. So what in that suggests an equivalent multiplier? > yet hard to write provably correct software 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. |
|
|
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.