Proofs as programs

ABSTRACT

The significant intellectual cost of programming is for problem solving and explaining, not for coding. Yet programming systems offer mechanical assistance for the coding process exclusively. We illustrate the use of an implemented program development system, called PRL ("pearl"), that provides automated assistance with the difficult part. The problem and its explained solution are seen as formal objects in a constructive logic of the data domains. These formal explanations can be executed at various stages of completion. The most incomplete explanations resemble applicative programs, the most complete are formal proofs.

REFERENCES

• 1: Dale Miller , Eve Longini Cohen , Peter B. Andrews, A Look at TPS, Proceedings of the 6th Conference on Automated Deduction, p.50-69, June 07-09, 1982
• 2: Joseph Louis Bates, A logic for correct program development, 1979
• 3: BATES, J., AND CONSTABLE, R.L. Definition of Micro-PRL. Tech. Rep. TR 82-492, Computer Science Dept., Cornell Univ., Oct. 1981.
• 4: BISHOP, E. Foundations of Constructive Analysis. McGraw-Hill, New York, 1967.
• 5: BISHOP, E. Mathematics as a numerical language. In Intuitionism and Proof Theory. J. Myhill, et al., Eds., North-Holland, Amsterdam, 1970, 53-71.
• 6: BLEDSOE, W. Nonresolution theorem proving. Artif Intell. 9 (1977), 1-36.
• 7: BOYER, R. S., AND MOORE, J.S. A Computational Logic. Academic Press, New York, 1979.
• 8: Alan Bundy, The computer modelling of mathematical reasoning, Academic Press Professional, Inc., San Diego, CA, 1985
• 9: CONSTABLE, R.L. Constructive mathematics and automatic program writers. In Proceedings of IFIP Congress, (Ljubljana, 1971), 229-233.
• 10: CONSTABLE R. L., AND BATES, J. L. The nearly ultimate PRL. Dept. of Computer Science Tech. Rep. TR 83-551, Cornell Univ., Apr. 1983.
• 11: CONSTABLE R.L. Intensional analysis of functions and types. Dept. of Computer Science Internal Rep. CSR-118-82, Univ. of Edinburgh, June 1982.
• 12: Robert L. Constable , Daniel R. Zlatin, The Type Theory of PL/CV3, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.94-117, Jan. 1984 [doi>10.1145/357233.357238]
• 13: R. L. Constable , S. D. Johnson , C. D. Eichenlaub, An Introduction to the PL/CV2 Programming Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 14: CONSTABLE R.L. Programs as proofs. Inf. Process. Lett. 16, 3 (Apr. 1983), 105-112.
• 15: DEBRUIJN, N. G. A survey of the project AUTOMATH. In Essays on Combinatory Logic, Lambda Calculus, and Formalism. J. P. Seldin and J. R. Hindley, Eds., Academic Press, New York, 1980, 589-606.
• 16: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 17: GORDON, M., MILNER, R., AND WADSWORTH, C. Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science, 78, Springer-Verlag, New York, 1979.
• 18: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 19: J. R. Guard , F. C. Oglesby , J. H. Bennett , L. G. Settle, Semi-Automated Mathematics, Journal of the ACM (JACM), v.16 n.1, p.49-62, Jan. 1969 [doi>10.1145/321495.321500]
• 20: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 21: JUTTING, L.S. Checking Landau's "Grundlagen" in the AUTOMATH system. Ph.D. dissertation, Eindhoven Univ., Math. Centre Tracts No. 83. Math. Centre, Amsterdam, 1979.
• 22: KLEENE, S.C. On the interpretation of intuitionistic number theory. JSL 10 (1945), 109-124.
• 23: KLEENE, S.C. Introduction to Metamathematics. D. Van Nostrand, Princeton, N.J., 1952.
• 24: Dean Blackmar Kraft, Avid: a system for the interactive development of verifiably correct programs, 1981
• 25: LAKATOS, I. Proofs and Refutations. Cambridge University Press, Cambridge, 1976.
• 26: Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
• 27: MARTIN-LOF P. Constructive mathematics and computer programming. In 6th International Congress for Logic, Method, and Philosophy of Science, (Hannover, Aug. 1979).
• 28: Bengt Nordström, Programming in Constructive Set Theory: Some examples, Proceedings of the 1981 conference on Functional programming languages and computer architecture, p.141-154, October 18-22, 1981, Portsmouth, New Hampshire, United States [doi>10.1145/800223.806773]
• 29: Lawrence Paulson, Deriving structural induction in LCF., Proc. of the international symposium on Semantics of data types, p.197-214, July 1984, Sophia-Antipolis, France
• 30: POLYA, G. How To Solve It. Princeton University Press, Princeton, N.J., 1945.
• 31: PROOFROCK, J. A. PRL: Proof refinement logic programmer's manual (Lambda PRL VAX version). Computer Science Dept., Cornell Univ., 1983.
• 32: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 33: SCOTT, D. Constructive validity. In Symposium on Automatic Demonstration. Lecture Notes in Mathematics, 125. Springer-Verlag, New York, 1970, 237-275.
• 34: Robert E. Shostak , Richard L. Schwartz , P. M. Melliar-Smith, STP: A Mechanized Logic for Specification and Verification, Proceedings of the 6th Conference on Automated Deduction, p.32-49, June 07-09, 1982
• 35: Robert E. Shostak, A Practical Decision Procedure for Arithmetic with Function Symbols, Journal of the ACM (JACM), v.26 n.2, p.351-360, April 1979 [doi>10.1145/322123.322137]
• 36: STENLUND, S. Combinators, Lambda-Terms, and Proof-Theory. D. Reidel, Dordrecht, 1972.
• 37: Tim Teitelbaum , Thomas Reps, The Cornell program synthesizer: a syntax-directed programming environment, Communications of the ACM, v.24 n.9, p.563-573, Sept. 1981 [doi>10.1145/358746.358755]
• 38: WHITEHEAD, A. N., AND RUSSELL, B. Principia Mathematica. Vol. 1, Cambridge University Press, Cambridge, 1925.
• 39: Niklaus Wirth, Systematic Programming: An Introduction, Prentice Hall PTR, Upper Saddle River, NJ, 1973
• 40: Wos, L., OVERBEEK, R., EWING, L., AND BOYLE, J. Automated Reasoning. Prentice-Hall, Englewood Cliffs, N.J., 1984.

INDEX TERMS

Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.2 Automatic Programming

          Nouns: PRL
  D.2 SOFTWARE ENGINEERING

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE

General Terms:
Algorithms, Design, Languages, Theory, Verification