Comment by paxy
9 hours ago
All this is going to do is move the problem up one layer. Sofware is fundamentally a representation of human expectations for the computer. How do you formally verify that?
9 hours ago
All this is going to do is move the problem up one layer. Sofware is fundamentally a representation of human expectations for the computer. How do you formally verify that?
Nohow, because the real world is informal. This is as far as coding can and will ever go, basically.
And like yes, it does just launder defects to a layer higher, but another way to phrase that in this case (and in many other cases) is that it raises the bar.
Instead of defects being mostly about nonsense minutia (relative to business logic), they are about actual design decisions and their correspondence to reality, i.e. the actual original goal and point of this god forsaken, navel-gazing field.
You do it by comparing to something that is “known” to be good.
I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.
Proving two things are equivalent is a major component of formal.
For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.
A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.