Logic In Programming

Not to be confused with LogicProgramming!

Floyd, Knuth, Hoare, Dijkstra, Jackson, Gries, Lamport, and many others have all argued that logic is a key to reasoning correctly about software.

This easy to prove since logic is the study of reasoning correctly in general, and reasoning about programs is just a special case.

The real question is whether it is worth reasoning about programs or should we rely on tests?

-- DickBotting

If you have no good semantics for how the programming language, standard library and operating system work, then tests are all that you can do. This is the major reason that's all people have been doing. Using reasoning has a high cost up front. However, there are cases where it would be much easier to reason something through than to do sufficiently exhaustive testing.

There is certainly an issue of low-hanging fruit. Where reasoning about programs (or sub-programs) is no more difficult than performing the tests, why not use reasoning? There are things that are difficult or impossible to test directly, such as spatial-temporal performance guarantees needed for critical aviation software. Beyond that, it's a matter of degree... you need to use logic to figure out the right tests, so why couldn't you just statically assert the test in the first place? If you're dealing with funky and unspecified systems like JavaScript keyboard events across browsers (http://unixpapa.com/js/key.html), how the frell do you even start to use logic?

I agree with your comments. Dijkstra has a nice article about testing a checkers board to see if we can make 31 pieces fit into a shape that 62 pieces can fit into. It is simple, easy, and fast to prove whether or not it is possible (using logic and reasoning), and testing each and every checkers board position would be completely wasteful and time consuming. In very many cases: reason, testing, and experimentation must be used rather than just testing.

[Experimentation and observation is something scientists and mathematicians have been doing for years. The arrogant idea that Dijkstra and similar fellows do not fill in values and test their theories and proofs is what leads people to this testing advocacy above (Python programmer for Bit Torrent has similar one sided advocacy issues). Use both testing and formal methods - not one or the other. Samuel has explained this, Lars has explained this - and we still have these people claiming that we can do only testing which is nonsense. During rocket ship design or operating system design, you do have some idea that people will be flying the rocket, going to planets, clicking buttons. Let's be realistic. One cannot claim that tests are all that you can do, without being laughed at.]

As with WesternCivilization, I think logic in programming would be a good idea.