Topic: program proving is infeasible

topics > computer science > programming > Group: program proving

requirement specification

automated tests of specifications and designs
consistency testing
embedded systems
error safe systems
formal methods and languages
hardware vs. software
limitations of formalism
limitations of system security
mathematical proof as a social process
model checker
problems with logic programming
program source as truth
specification is infeasible


Program proofs are notorious for their length, complexity and error proneness. Only highly trained researchers have attempted proofs of any size. There are several weaknesses: (1) Program proving is an isolated phenomenon used as a formal exercise. It is unlike mathematics where proofs are used to simplify and provide foundations for further development. (2) Proofs are only possible if the program is already correct. They will not show where a program is incorrect nor do they indicate incorrect programs. (3) Proofs are dependent upon a correct specification of criterion. A proof only demonstrates a consistent program representation, not a representation which is valid, maintainable, useful, and efficient. (cbb 5/80)

Program proofs ignore the possibility of errors in the program's environment. A proof may be too costly, and it may encourage the removal of useful redundancies. In short, proving a program does not make the program trustworthy. Program proofs remain a useful consistency check for safety-critical programs. (cbb 12/92)

Subtopic: practical formal methods up

Quote: use formal methods to verify a design instead of proving correctness; forces engineers to be precise about details; resolves differences of interpretation between implementers and testers [»tretJ9_2001]
Quote: program proving and automatic derivation of code from formal specifications are not important; e.g., implementation of formal specifications caused few errors [»tretJ9_2001]

Subtopic: problem of reliability and trustworthiness up

Quote: a verified program is provably corrected but not reliable and trustworthy; no information about limits [»demiRA5_1979]
Quote: nothing can prove the absence of bugs; verification can not prevent failures from unforeseen causes [»abraP12_1986]
Quote: program verification does not provide reliability, safety, or security; it proves limited design correctness [»dobsJ4_1989]

Subtopic: proof as consistency checking up

Quote: logic is not flexible enough for thinking because consistency is too strong a requirement [»minsM_1981]
Quote: validation methods are primarily used as bug-finders; formal methods are useful because they find different bugs than traditional methods; a more realistic goal than guaranteeing correctness [»dillDL4_1996]
Quote: proving a hardware design is just another form of checking; does not catch specification errors and analog behavior [»wilkM10_1990]
Quote: program verification useful for clarifying specifications and removing design faults; not for guaranteed correctness [»dobsJ4_1989]
Quote: instead of 'proof of correctness', should use 'proof of relative consistency'
Quote: consistent, closed, complete methods are limited for elucidating truth [»gammRC10_1974]
Quote: a program proof is for refutation of certain forms of incorrectness; math proofs demonstrate existence [»dobsJ4_1989]

Subtopic: problem of specification errors up

Quote: uncaught errors in executable specification languages are just as disastrous as in traditional programming [»abboRJ3_1990]
Quote: neither structured programming nor proofs of correctness attempt to check the specification itself [»bateD_1976]
Quote: proof may show that a program matches its specifications, but does not tell if the specifications are correct [»gammRC10_1974]
Quote: a formal specification also requires user feedback from an implementation [»abboRJ3_1990]
Quote: a program can be wrong only because the customer wanted a different function to be calculated [»scowRS3_1982b]
Quote: only testing reveals discrepancies between a model and the real situation; also errors in proofs [»parnDL6_1990]

Subtopic: proof is social up

Quote: an important part of 'proof' in mathematics is the social mechanism; does not exist for proving programs [»demiRA_1977]
Quote: simple, unspecialized theorems become part of mathematics, but program proving produces narrow theorems for a paltry class of structures [»demiRA_1977]
Quote: a verification of a program must be accepted blindly without the social processes of mathematical proofs [»demiRA5_1979]
Quote: a verification may not be transferable to any other program; prevents social processes [»demiRA5_1979]
Quote: the details of the proof of Smallintset are complex and not included with this paper [»hoarCA_1972a]

Subtopic: engineers do not prove up

Quote: there are no proofs that bridges stand, that airplanes fly, or that power systems deliver electricity
Quote: in a mature engineering discipline, 'reliable' never means 'perfect' [»demiRA_1977]
Quote: in formal methods there is an unreasonable focus on proof of correctness; in other areas, engineers use mathematics to derive important properties such as the maximum voltage between two terminals [»parnDL4_1996]

Subtopic: proof not possible up

Quote: since a program is a human artifact it will contain imperfections and can never be verified [»demiRA5_1979]
Quote: a program is the only complete description of the program's behavior [»demiRA5_1979]
QuoteRef: cbb_1973 ;;11/3/74 one can not prove a space of representation

Subtopic: problem of exceptions up

Quote: analyzing exceptions for correctness is difficult [»cargT11_1994]

Subtopic: problem of invalid data up

Quote: program verification assumes that nonsensical operations do not occur; i.e., data is valid [»stroRE1_1986]

Subtopic: problem of side-effects up

Quote: languages in which erroneous programs have arbitrary side-effects are non-secure because every module must be proven error free before any can be [»stroRE5_1985]

Subtopic: problem of feature interaction up

Quote: feature interaction makes program validation complicated [»wassAI3_1979]

Subtopic: problem of efficiency up

Quote: full formal development with machine-checked proofs is too expensive except for failure-critical applications
Quote: model checkers find a few difficult errors with simplified code; meta-level compilation works directly with program source and found many errors [»chouA11_2000]
Quote: reliability is only one of many desired properties; high reliability may cost too much [»gammRC10_1974]
Quote: the construction of symbolic structures uses resources; can be impossibly long if care is not taken [»demiRA5_1979]
Quote: proofs with a general purpose theorem prover may almost always be impractically long [»rabiMO8_1974]
Quote: there are always short true statements concerning the addition of natural numbers whose formal proof is super-exponentially long [»rabiMO8_1974]

Subtopic: problem of finding invariants up

Quote: proving program correctness depends on knowing the invariants satisfied by the program; given a complicated program may be difficult to find [»baueFL_1976]
Quote: it is hard to find 'the' invariant when a program is wrong [»baueFL_1976]
Quote: Hoare axioms exist for at most 4 of 5 block-structured features: procedure parameters, recursion, static scope, globals, internal procedures [»clarEM1_1979]

Subtopic: program verification not done up

Quote: program proofs, cross-references, attribute lists, and dumps were rarely used
Quote: program verification is a shared joke among programmers; something that must be learned and then ignored

Subtopic: proof removes redundancies up

Quote: if we feel that something is provably right then redundancies are removed [»demiRA5_1979]

Subtopic: successful proof checking up

Quote: certified evaluation via a proof checker for lists of facts, security rules, and derivations; 100 lines of code [»jimT5_2000]
Quote: verifying a finite state model is much easier that fully understanding a system's behavior; e.g., only four operations on user IDs

Related Topics up

Group: requirement specification   (11 topics, 307 quotes)
Group: testing   (18 topics, 557 quotes)

Topic: automated tests of specifications and designs (12 items)
Topic: consistency testing (60 items)
Topic: embedded systems (26 items)
Topic: error safe systems (76 items)
Topic: formal methods and languages (53 items)
Topic: hardware vs. software (15 items)
Topic: limitations of formalism (93 items)
Topic: limitations of system security (39 items)
Topic: mathematical proof as a social process (14 items)
Topic: model checker (49 items)
Topic: problems with logic programming (10 items)
Topic: program source as truth (17 items)
Topic: specification is infeasible
(46 items)

Updated barberCB 11/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.