Hacker News Reader

The article's not silly. Leveson and Hamilton's works cover that explicitly. Start with Engineering a Safer World's Intent Specifications, move on to Safeware, and look at the attention that goes into writing the right TLA+ specs.

Lists like "Government regulations, flaky hardware…" look a lot like the upper levels of the hierarchical control systems contemplated there. It didn't make it into a pop science piece, but it's absolutely core to the work at issue.

You can get a copy of the book at http://sunnyday.mit.edu/safer-world/index.html .

It sounds like you're both in agreement, which would support the criticism of the article, which hides the (addressing of the) very points the parent was raising, and gives the impression that it only solves the very academic version of the problem rather than the real-world software snags.

Everything you said after "this article is silly" kinda seems like just restating the exact point of the article.

The central idea is that the massive costs of writing code that adheres to a specification takes away resources from the task of understanding the problem space well enough to create a correct specification. That is, incidental complexity overwhelms essential complexity in modern software engineering. The various avenues of study mentioned in the article are attempts at addressing that imbalance.

Which is pretty much what you said.

You cannot explore problem space without writing code for it. But once you have you spaghetti code how do you rewrite it to align with your new understanding? And what happens if you enhance your understanding even better while doing rewrite?

> Government regulations, flaky hardware, network latency, human error, financial limits, competition, malicious actors, gamma rays, other people's software, power outages, terrorists, dependencies, operating system upgrades, corrupt data, hurricanes, all are conspiring against your software. Can you plan for all of that?

If your answer to all of those is, "No, I can't, so I won't bother, we'll just update the software later," then please excuse yourself from designing anything of consequence and stick to making websites that gobble dollars from advertising, because planning for those things, ahead of time, quantifying them, and being ready, is _absolutely_ the job of engineers, and you're derelict of duty if you don't.

skywhopper gets it exactly right!

I think the software development community needs to do much more to explain exactly this to the other communities that interact with us, the managers, program/process managers, users, etc.

We have to ensure people understand that the hardest part of software engineering isn't really the coding the software itself, but discovering what the actual problem(s) to be solved are and what is the constraint space of the solution(s). And I call it discovery because I assert no one, up to the point software engineers got involved, ever thought to detail exactly all those things.

It's not a one size fits all thing. The majority of startups won't need these methods, think software for examples in the article: control systems, critical infrastructure, etc. It's fine to have different approaches for different classes of software. Raising awareness of these tools is critical because most software engineers haven't put much thought into them.

I think you might enjoy this paper, I did: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf

I think this paper is quite wrong, and has already been shown to be wrong by all the people who have successfully applied formal methods to their projects.

We believe that, in the end, it is a social process that determines whether mathematicians feel confident about a theorem — and we believe that, because no comparable social process can take place among program verifiers, program verification is bound to fail.

This overlooks the fact that the verifiers aren't black boxes; people trust the TLA+ tools and Coq and Isabelle and PVS because the principles by which they work are well understood, and on top of that, these tools are all open source. (If someone developed a closed-source verifier, they could still leverage this trust by making their verifier output proofs in a format that could be checked by one of these.) So while the individual proofs generated in a software verification are probably not going to be checked socially -- they're mostly just not interesting enough -- there is still a social process operating at the meta-level that gives us confidence in them.