The points you're raising are not what I'm arguing.
What I am arguing is this:
Formal verification only guarantees consistency between the 'specification' and the 'implementation.' It does not guarantee that the 'specification' correctly reflects reality. This is a problem of modeling.
For your logic to hold, it would imply that humans can formalize, to some degree, the amount of loss that occurs when modeling reality. That is not possible.
It only tells you whether the implementation satisfies the specification. That's also what the OP's post is about. The point that 'the cost has been lowered due to AI' is largely no different from simply saying 'the cost of implementation has gone down.' The real question is whether that implementation properly reflects reality.
The OP's post is fundamentally about 'internal invariants.'
But if you look at the beginning of the first post: 'But outside of some special cases (notably, hardware synthesis), our sense has been that formal methods were just not worth the costs for us. And those costs are really high! seL4 is a great example of this. It's a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.' And the post suggests extending existing methodologies. I think a limited case and generalizing it are different problems. The point is that not every special case is general.
That is why I pointed out whether this extension of methodology is even possible. I am skeptical on this point.
If you want to criticize me, rather than talking about such methodologies, you should criticize the essence of my logic: whether even offensive programming properly understands modeling. I am not simply opposing the OP's post; rather, I am asking whether modeling in the age of AI agents is comparable to modeling in the past.
The materials you shared for me are helpful, but I am saying they do not align with my logic.
Your introduction says: '===== The Problem: Realism vs. Idealism =====' Right?
The question is whether the idealism you advocate actually reflects reality. I am simply arguing for modeling. The gap in my argument is that 'then, because modeling also changes frequently, couldn't all methodologies become useless?' That could be a potential flawed skepticism. But what you're saying is not that.
Every argument has a blind spot. But you are not reading the weak points of my argument; you are only reading your own strong points. This only creates friction and leads us to argue about our emotional differences. I think you are intelligent and knowledgeable. But the points you're raising are not the points of criticism I intended, and what you're pointing out is not what I said.
I am not saying that all methodologies are wrong. I am saying that a methodology can go wrong if it steps outside its boundaries.
However, the fact that you linked me to things I could study was, I think, a gesture of goodwill, assuming that I, as a junior programmer, was misunderstanding something and trying to help me learn. But criticism that assumes I just don't understand isn't helpful for either of us.
