5 ms·

This article is silly in a lot of ways. The real problem of software engineering is not "how do you prove this code follows algorithm X exactly?" It's "how do y

This article is silly in a lot of ways. The real problem of software engineering is not "how do you prove this code follows algorithm X exactly?" It's "how do you know what algorithm X needs to be in sufficient detail to implement it?" It's "when you realize you were wrong about algorithm X, how do you change your existing, working code to implement the new algorithm X-prime, without interruption?" It's "what do we do when we realize algorithm X-prime was completely the wrong thing, and now we need to transition to algorithm Y, and also fix all the data that algorithm X-prime messed up?" No matter what awesome tool you come up with to translate requirements into CPU bytecode, you still have to translate human requirements into that requirements language, whether that language is assembly, C, Java, Rust, Haskell, or TLA+. When you have the money and time and patience to fully examine the problem space and work out exactly what the requirements are, that's great. In the far more common scenario, you have impatient investors, or you're inventing something entirely new, or your software will deal with the real world which is not as predictable as an imaginary algorithm. 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?

haskellandchill 9y ago
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.
brians 9y ago
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 http://sunnyday.mit.edu/safer-world/index.html .
- SilasX 9y ago
  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.
arximboldi 9y ago
I think you might enjoy this paper, I did: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf
- ScottBurson 9y ago
  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.
gipp 9y ago
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.
- kikimora 9y ago
  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?
jgeada 9y ago
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.
titzer 9y ago
> 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.

haskellandchill 9y ago

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.

brians 9y ago

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 http://sunnyday.mit.edu/safer-world/index.html .

SilasX 9y ago
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.

arximboldi 9y ago

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

ScottBurson 9y ago
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.

gipp 9y ago

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.

kikimora 9y ago
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?

jgeada 9y ago

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.

titzer 9y ago

> 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.