[jdw64]

You're right. I think the point we need to discuss here is, to be clear, dividing the contexts in which defensive programming is strong and where it should be aggressive.

I think the overhead of implementation is enormous, but I believe AI can write it. However, before even reaching the 'implementation' stage, that is, at the planning stage, sufficient data must be collected for the implementation to be safe.

In that respect, I think Jane Street already has enough data and modeling capabilities. However, I think it's a bit difficult to say whether this approach will take shape in many other domains.

In that sense, I also think that the reason many industries are doing this kind of fast deployment and experimental tooling might be a preparatory step for that kind of modeling. Have a good day Thanks for the good comment. It helped me think more sharply as well

[majormajor]

> I think the overhead of implementation is enormous, but I believe AI can write it. However, before even reaching the 'implementation' stage, that is, at the planning stage, sufficient data must be collected for the implementation to be safe.

I don't really follow here, I think once you know what you want the system to do, you could start to model it formally. What data do you think needs collection for planning here? Is it just for performance profiling of whatever algorithms are decided on? But that seems equally as relevant as if you do your initial implementation straight-up in code w/o any formal approach.

[jdw64]

Formal verification is a mathematical proof and requires axioms. However, if real world field data is not collected, you are not comparing theory to reality but forcing reality to fit the theory, like the bed of Procrustes.

This means the object of verification is not reality but the consistency between specification and implementation, and incorrect formal verification only refines a wrong worldview.

A company with sufficient capital can turn a theory into reality through marketing and other means. But for small businesses or in markets where new competitive logic is introduced due to the lifespan of an industry, this can be a fatal problem.

For example, consider the stock market. If you use the Buffett indicator to invest right now, the market looks overheated. But other indicators suggest positive prospects. We cannot know whether the market logic of the AI era aligns with the past or is different, but I believe there are cases where modeling changes due to real world shifts.

In reality, when converting the real world into mathematics or physics, information loss is inevitable. In this process, science may later advance and become more precise, or a value once considered important may turn out to be wrong.

In other words, something may be correct within a given set of axioms, but those axioms themselves may change depending on the context. The history of computer standards has shown this as well(ASCII -> Unicode)[To explain this point, ASCII works perfectly in English speaking countries, but in my country it creates incorrect encoding.]

Programmer's ability may come down to distinguishing between what changes little and lasts long, and what changes quickly

After writing the replt, I realized I was being too critical of formal verification. I think Jane Street's argument holds for invariants inside code. However, I am cautious about whether that logic can be extended to other fields. I haven't studied deeply enough, so my thinking may be shallow. Please understand