Social processes and proofs of theorems and programs

ABSTRACT

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.

REFERENCES

• 1: Baker, F.T. Chief programmer team management of production programming. IBM Syst. J. 11, 1 (1972), 56-73.
• 2: Cohen, P.J. The independence of the continuum hypothesis. Proc. Nat. Acad. Sci., USA. Part I, vol. 50 (1963), pp. 1143-1148; Part II, vol. 51 (1964), pp. 105-110.
• 3: Davis, P.J. Fidelity in mathematical discourse: Is one and one really two? The Amer. Math. Monthly 79, 3 (1972), 252-263.
• 4: Bateman, P., and Diamond, H. John E. Littlewood (1885-1977): An informal obituary. The Math. lntelligencer 1, l (1978), 28-33.
• 5: Gelerenter, H., et al. The discovery of organic synthetic roots by computer. Topics in Current Chemistry 41, Springer-Verlag, 1973, pp. 113-150.
• 6: John Alan George, Computer implementation of the finite element method, 1971
• 7: Thomas L. Heath , Euclid, The Thirteen Books of Euclid's Elements, Books 1 and 2, Dover Publications, Incorporated, 1956
• 8: Heawood, P.J. Map colouring theorems. Quarterly J. Math., Oxford Series 24 (1890), 322-339.
• 9: Hoare, C.A.R. Quoted in Software Management, C. McGowan and R. McHenry, Eds.; to appear in Research Directions in Software Technology, M.I.T. Press, Cambridge, Mass., 1978.
• 10: Jech, Thomas J. The Axiom of Choice. North-Holland Pub. Co., Amsterdam, 1973, p. 118.
• 11: Kempe, A.B. On the geographical problem of the four colors. Amer. J. Math. 2 (1879), 193-200.
• 12: Kolata, G. Bail. Mathematical proof: The genesis of reasonable doubt. Science 192 (1976), 989-990.
• 13: Lakatos, Imre. Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press, England, 1976.
• 14: Manin, Yu. I. A Course in Mathematical Logic. Springer-Verlag, 1977, pp. 48-51.
• 15: Meyer, A. The inherent computational complexity of theories of ordered sets: A brief survey. Int. Cong. of Mathematicians, Aug. 1974.
• 16: G. J. Popek , J. J. Horning , B. W. Lampson , J. G. Mitchell , R. L. London, Notes on the design of Euclid, Proceedings of an ACM conference on Language design for reliable software, p.11-18, March 28-30, 1977, Raleigh, North Carolina
• 17: Rabin, M.O. Probabilistic algorithms. In Algorithms and Complexity: New Directions and Recent Results, J.F. Traub, Ed., Academic Press, New York, 1976, pp. 2140.
• 18: Schwartz, J. On programming. Courant Rep., New York U., New York, 1973.
• 19: Stockmeyer, L. The complexity of decision problems in automata theory and logic. Ph.D. Th., M.I.T., Cambridge, Mass., 1974.
• 20: Ulam, S.M. Adventures of a Mathematician. Scribner's, New York, 1976, p. 288.

INDEX TERMS

Keywords:
formal mathematics, mathematical proofs, program specification, program verification