I don't think there's any way to ask a very precise question here, so this might be considered opinion based. Nevertheless, it seems the question is clear enough because I'm asking whether these two initial steps towards a theory are trying to achieve the same thing. It seems to me Hoare went towards an imperative-calculus and McCarthy went towards a functional-calculus for deriving programs hand in hand with mathematical proofs. Can we say they both went towards that each in different (imperative, functional) ways?

I'm comparing A Basis for a Mathematical Theory of Computation by John McCarthy with An Axiomatic Basis for Computer Programming by Sir Charles Anthony Richard Hoare.

To me the main contribution (or the most interesting part) of McCarthy's paper is given in section 3.2, recursion induction, where he exemplifies how one can prove two algorithms being equivalent --- algorithms as specified by the language defined in the paper. (I possibly have this opinion because to me so much of his work is no news, since I'm familiar with Lisp and recursion.)

My understanding it at least partially confirmed by what he says right in the introduction [introduction, point 2, page 2].

To define a theory of the equivalence of computation processes. With such a theory we can define equivalence preserving transformations. Such transformations can be used to take an algorithm from a form in which it is easily seen to give the right answers to an equivalent form guaranteed to give the same answers but which has other advantages such as speed, economy of storage, or the incorporation of auxiliary processes.

Extra-credit. It seems Dijkstra followed along Hoare's approach because even after the 70s he kept on using precisely Hoare's notation, introduced in Hoare's paper in 69. I would appreciate answers also linking Dijkstra's opinion on the matter --- although really not required.

  • 2
    $\begingroup$ Recommended reading for McCarthy's bluntness alone, e.g.: "Lack of such a formalism is one of the main weaknesses of ALGOL, but the business data processing languages such as FLOWMATIC and COBOL have made a start in this direction, even though this start is hampered by concessions to the presumed prejudices of business men." or "We hope that the reader will not be angry about the contrast between the great expectations of a mathematical theory of computation and the meager results presented in this paper." $\endgroup$
    – Kai
    Feb 2 '19 at 9:12
  • 1
    $\begingroup$ Comparing the version of McCarthy's paper you linked to the original 1961 paper, suggests that some typos crept into the OCR. On the other hand, that 1963 version promises an additional 10th section (labelled 4.2). $\endgroup$
    – Kai
    Feb 2 '19 at 9:22
  • $\begingroup$ This question seems more appropriate for hsm.SE. Possibly the question could be migrated? $\endgroup$ Jan 3 '20 at 21:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.