Reading through the chapter of mathematical reasoning in the B Book, I couldn't help but notice how much emphasis was put in using natural deduction. I strengthening the belief that natural deduction is not appropriate as it is for practical reasoning. In fact, I think it is appropriate to compare it to Turing machines. When we are interested in the power of a system, we want to reduce it to its bare essential. In that sense, the few simple inference rules usually associated with natural deduction are very helpful. But we must keep in mind the bias that we have when delivering that judgment: we are doing the job of a logician who wants to compare different systems. It is the same for Turing machines. They are very simple and this is why it helps reasoning about their computability properties. I think nobody knowing anything about programming would suggest to use a Turing machine to build any kind of useful system unless it is sufficiently small as to be of no significance.
Similarly, I don't think that using natural deduction as a means for reasoning about systems is any wiser than programming with Turing machines. For simplifying the logic, natural deduction offers no means to exploit equivalence because it can be dealt with using implication. It is true but not helpful when carrying out an actual reasoning. Keeping equivalence intact is simply much more efficient. People don't have to go through the same proof twice. It is also true that even if case analysis can help achieve the proof, it also helps making it unmanageable.
In short, developing proof design techniques is as necessary as developing program design techniques and, similarly, it involves developing the right notation and finding powerful heuristics. Natural deduction is not a means to that end. However, it can be used to prove properties of equational logic without to need use it when carrying out the actual reasoning.
Simon Hudon Zürich June 9th, 2009
