Under the spell of Dijkstra's dream

I find Edsger W. Dijkstra's talk "How Computing Science created a new mathematical style", recorded in the manuscript EWD1073 one of his most beautiful. Not only is it a clear exposition of his calculational approach to mathematics, to me it is especially poignant since it carries with it the weight of thirty years of experience with the discipline. As such is not so much a promotional piece as a survey of results.

Many things in this talk struck me as worthy of reflection; one thing that stood out was the two examples he gave of how computer science informed (or ought to inform) mathematical discipline:

In order to prove that a compiler correctly parses the program texts it processes, one needs a formal grammar for the syntax of the programming language in question. To formal language theory we owe the distinction between grammars that are "context-free" and those that are not. Next we observe that the manipulating mathematician does not manipulate just strings of symbols but manipulates formulae parsed according to the underlying grammar. Since the parsing problem is simpler for context-free grammars, the moral is simple: choose for one's formalisms context-free grammars.

The other example is the notion of abstract data types —stacks, trees, permutations, bags, configurations, what have you—. Identifying an appropriate data type and some operations on it is often essential in preventing a program from becoming totally unwieldy. In exactly the same way calculational proofs of the desired brevity and clarity can often be obtained by the use of a specifically designed, special-purpose calculus. I said "exactly the same way" because I see no difference between the virtues of a data type in a program and the virtues of a calculus in a proof.

Much is written nowadays about how DSLs enhance the quality of code in complex systems; here is a forceful argument about DSLs enhancing mathematical reasoning.

As an example of this, and because I felt absolutely in awe at the simplicity and transparence of the proof and I think it deserves to be repeated, here is Dijkstra's proof of the Induction Principle:

Theorem: (C, <) is well-founded if and only if mathematical induction over C with respect to < is a valid proof technique.

  (C, <) is well-founded
≡ { definition of well-foundedness }
  (∀ S :: (∃ x :: x ∈ S) ⇒ (∃ x :: x ∈ S ∧ (∀ y : y < x : y ∉ S)))
≡ { contrapositive and Laws of de Morgan }
  (∀ S :: (∀ x :: x ∉ S) ⇐ (∀ x :: x ∉ S ∨ (∃ y : y < x : y ∈ S)))
≡ { transforming the dummy: S = { x | ¬P.x }, P.x ≡ x ∉ S }
  (∀ P :: (∀ x :: P.x) ⇐ (∀ x :: P.x ∨ (∃ y : y < x : ¬ P.y)))
≡ { predicate calculus }
  (∀ P :: (∀ x :: (∀ y : y < x : P.y) ⇒ P.x) ⇒ (∀ x :: P.x))
≡ { definition of proof via mathematical induction }
  mathematical induction over (C, <) is valid