I'm aware, but I'm more talking about theoretical computer science than practical software and systems engineering. Methods for formal verification and design o

I'm aware, but I'm more talking about theoretical computer science than practical software and systems engineering. Methods for formal verification and design of software are of course interesting, but quite different from formal verification of theory. What I wanted to point out is that even a very formal field (advanced, pure math) is still plagued by very mundane and very human logical errors. Further, these errors are not easily spotted by machine, at least not with current technology. Regarding Dijkstra, I personally consider TCS to be a branch of applied math or maybe applied logic. What most programmers do in practice, however, is more akin to engineering (or I'd say, is a type of engineering).