[fultonn]

I think every formal methods phd student who's interested in adoption of their techniques/tools has a short bout of doubt/depression upon realizing just how large of a surface area for bugs lives in a sufficiently useful specification.

This is deeply related to the conceptual error a lot of executives are currently making around automation in/of their software engineering orgs.

It has always been true that learning some formal methods probably makes you a better programmer in certain ways, even if you never use them. I think it's increasingly also true that learning some formal methods probably makes you a better manager of people/processes that product software.

[shermantanktop]

Execs will often hand-wave away complexity as being irrelevant detail. And sometimes it is - especially if an urgent directional decision is needed.

The key skill - which is rare - is knowing exactly how much analysis to do.

Formal methods are appealing because they suggest that full analysis is possible. But formally proved programs can still have bugs!

[fultonn]

I think you probably got this, but spelling it out anyways for future readers.

The conceptual gap I'm referring to here has nothing to do with formal methods per se. It's just an analogous problem with the quanta of information required to state the spec vs the quanta of information required to state the implementation.

Namely: once your problem has enough of a certain type of essential complexity, there's not a huge delta between "a sufficiently specific description of the problem" and "the source code that solves the problem". The complexity of a sufficiently specific prompt approaches the complexity of the actual solution. At that point, the former does not have the purported benefit and the latter has a lot of huge benefits (determinism, modularity, etc).

When one is operating in that regime of problems, proposing that one can substantially automate the software engineering function has a real "I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question" feel to it.

[teiferer]

Well put, thank you.

One thing I should say though is that the spec has the luxury of being free of some constraints that the implementation has. For example, the functional spec of a sorting function could describe the shape of the required output without having to say how to arrive there. Or in more complicated cases it could afford an exponential simple algorithm to say that the actual implementation must be functionally equivalent. That may make it simpler because it's free of having to run in linear or whatever time complexity.

[fultonn]

Yes, it's probably the most important trick in formal methods. Often surprisingly difficult to make it actually work, but when it does you can end up with a powerful tool.

In a past life I spent a lot of time on that sort of thing for control systems and RL. Spec says what not to do, reward says what to do, implementation can be arbitrarily complex wrt the spec.

There are many opportunities for an analogous move in LLM-assisted software engineering.

[shermantanktop]

Right, it's a map with a scale of 1:1.

A map with a scale of 100:1 is perfectly useful for navigation. It's just no good for specifying the terrain you want to build with any precision.