Dijkstra was advocating for using formal methods...

Do the people agreeing with the article agree with its actual point? Especially whether it was wise before AI (maybe) improved the practicality of such an undertaking?

Expressive type systems have all the hype nowadays.

Those absolutely global formal systems that can explain any kind of behavior would never be practical in general. But specialized formal systems are just great.

How much value is there in formal proof that a program optimally meets precisely-described requirements if the requirements themselves are sub-optimal for the problem area of concern?

In other words, "software is hard": https://www.gamearchitect.net/Articles/SoftwareIsHard.html "The difference is that the overruns on a physical construction project are bounded. You never get to the point where you have to hammer in a nail and discover that the nail will take an estimated six months of research and development, with a high level of uncertainty. But software is fractal in complexity. If you're doing top-down design, you produce a specification that stops at some level of granularity. And you always risk discovering, come implementation time, that the module or class that was the lowest level of your specification hides untold worlds of complexity that will take as much development effort as you'd budgeted for the rest of the project combined. The only way to avoid that is to have your design go all the way down to specifying individual lines of code, in which case you aren't designing at all, you're just programming. Fred Brooks said it twenty years ago in "No Silver Bullet" better than I can today: "The complexity of software is an essential property, not an accidental one. Hence, descriptions of a software entity that abstract away its complexity often abstract away its essence.""

I prefer a conceptual model more like "Software as Gardening". https://github.com/pdfernhout/High-Performance-Organizations... "Andy Hunt: There is a persistent notion in a lot of literature that software development should be like engineering. First, an architect draws up some great plans. Then you get a flood of warm bodies to come in and fill the chairs, bang out all the code, and you're done. A lot of people still feel that way; I saw an interview in the last six months of a big outsourcing house in India where this was how they felt. They paint a picture of constructing software like buildings. The high talent architects do the design. The coders do the constructing. The tenants move in, and everyone lives happily ever after. We don't think that's very realistic. It doesn't work that way with software. We paint a different picture. Instead of that very neat and orderly procession, which doesn't happen even in the real world with buildings, software is much more like gardening. You do plan. You plan that you're going to make a plot this big. You're going to prepare the soil. You bring in a landscape person who says to put the big plants in the back and short ones in the front. You've got a great plan, a whole design. But when you plant the bulbs and the seeds, what happens? The garden doesn't quite come up the way you drew the picture. This plant gets a lot bigger than you thought it would. You've got to prune it. You've got to split it. You've got to move it around the garden. This big plant in the back died. You've got to dig it up and throw it into the compost pile. These colors ended up not looking like they did on the package. They don't look good next to each other. You've got to transplant this one over to the other side of the garden. --- Dave Thomas: Also, with a garden, there's a constant assumption of maintenance. Everybody says, I want a low-maintenance garden, but the reality is a garden is something that you're always interacting with to improve or even just keep the same. Although I know there's building maintenance, you typically don't change the shape of a building. It just sits there. We want people to view software as being far more organic, far more malleable, and something that you have to be prepared to interact with to improve all the time."

And it helps to keep things simple. https://www.infoq.com/presentations/Simple-Made-Easy/ "Rich Hickey emphasizes simplicity’s virtues over easiness’, showing that while many choose easiness they may end up with complexity, and the better way is to choose easiness along the simplicity path."

Love the gist of this, but just wanted to point out, but there's no need to draw the line between buildings and gardening. Anyone who has built a house or done major remodel knows that it too suffers from fractal complexity. It may not be a nail that becomes a wormhole of complexity (as neither is something simple arithmetic operations in programming), but all kinds of things can crop up. The soil has shifted since last survey, the pipes from city are old, the wiring is out of date, the standards have changed, the weather got in the way, the supplies changed in price / specification, etc. Everything in the world is like that, software isn't special in that regard. In fact, software only has such complexity because its usually trying to model some real-world data or decision. For the totally arbitrary toy examples, the code is usually predictable, simple, and clean ; the mess starts once we try to fit it to real-world usecases (such as building construction).