Hacker News Reader

Comment by timkam | Hacker News Reader

From a computer science perspective, this is an interesting piece. But from a practical perspective, I doubt that the Dijkstra of 1988 has a good understanding of the sociotechnical reality of the present day software industry. I comment (quite obviously) not to disparage him and his outstanding achievements, but rather to highlight that we cannot expect that Dijkstra could predict the future, in particular in a realm that somewhat exceeds the domain of his expertise. For example, I think by now we have a good understanding of the relevance and importance of software maintenance. Sure, software is not "subject to wear and tear", but the world around software evolves and a program that did a job well 10 years ago might not to the same job well today (think about security). We all understand this difference; i.e., I don't think his nit-picky attacks on software engineering metaphors are particularly useful from today's perspective.

View on HN

He was an advocate of formal methods like Hoare Logic, which in principle could be used to write highly secure programs.

It's possible though that not all aspects of security can be addressed by formal methods. There's the issue of side-channel attacks (like SPECTRE), which are not easy to model using formal methods.

I think this is the difference between cs and software engineering. Two people can look at a problem (build secure programs). The cs person sees static analysis, model checking, and other mathematically principled approaches as the solution. The engineer sees a suite of human approaches (code review, testing, fuzzing, audits, etc). I think the pure cs vision is narrow and limits our ability to choose the best method to solve a problem for the minimal price. Formal methods should be like unit tests, a component of the software engineering process. But it should also be acceptable to acknowledge its role and limits, just like how we don’t rely exclusively on unit testing to deploy correct programs.

> It's possible though that not all aspects of security can be addressed by formal methods.

Well, one can always devise some well-defined model in which you can prove stuff. So nothing is ever unreachable.

> There's the issue of side-channel attacks (like SPECTRE), which are not easy to model using formal methods.

SPECTRE is not an error in programs, it's a breach of contract of the CPU (what shouldn't be observable actually is). I'm pretty sure formal methods would be of great help to design clean interactions between a speculative engine and the cache hierarchy. See eg https://plv.csail.mit.edu/kami/ from umbrella project deepspec.

One very common side-channel at program level (and probably one of the most important) is timing side-channel (and all derived: power draw, noise level etc). This one is "easily" solved (in the sense it's not an open research question): have constant-time function types. It's not hard discriminating between what's constant time and what's not: don't branch on input and execute only constant time primitives.

Reply on news.ycombinator.com