Social Processes and Proofs of Theorems and Programs. De Millo, R. A.; Lipton, R. J.; and Perlis, A. J. 22(5):271–280.
Social Processes and Proofs of Theorems and Programs [link]Paper  doi  abstract   bibtex   
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.
@article{demilloSocialProcessesProofs1979,
  title = {Social Processes and Proofs of Theorems and Programs},
  author = {De Millo, Richard A. and Lipton, Richard J. and Perlis, Alan J.},
  date = {1979-05},
  journaltitle = {Commun. ACM},
  volume = {22},
  pages = {271--280},
  issn = {0001-0782},
  doi = {10.1145/359104.359106},
  url = {https://doi.org/10.1145/359104.359106},
  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.},
  keywords = {*imported-from-citeulike-INRMM,~INRMM-MiD:c-939451,computational-science,epistemology,mathematical-reasoning,mathematics,semantics,software-engineering,software-errors,software-uncertainty},
  number = {5}
}
Downloads: 0