Wegner OOPSLA'95, " [...] formal correctness proofs have a limited role as evidence for the correctness of interactive systems."

[Massimo Dentico]

Another  citation from the paper  of Wegner  (emphasis is mine, of
course) and, after, some of my questions.

==================================================================
                                 
                OOPSLA Tutorial Notes, October 1995

        Tutorial Notes: Models and Paradigms of Interaction
          Peter Wegner, Brown University, September 1995
                                 
        (http://www.cs.brown.edu/people/pw/papers/oot1.ps)

[...]

3.1 Irreducibility and incompleteness

Gödel  incompleteness for the integers reflects the incompleteness
of  many  other  domains  whose sets of true  assertions  are  not
recursively enumerable, including that of interaction machines. It
strikes  a  blow against reductionism, and by implication  against
philosophical  rationalism.  The irreducibility  of  semantics  to
syntax,  which  is  considered  a  fault  from  the  viewpoint  of
formalizability,  becomes  a  feature  of  empirical   models   in
permitting  empirical semantics to transcend  the  limitations  of
notation.  Plato's despairing metaphor that our view of  the  real
world  consists of mere reflections of reality on the walls  of  a
cave was turned around by the development of empirical models that
predict  and  control  such  partially-perceived  reflections   of
reality.  Empirical  models  accept  inherent  incompleteness  and
irreducibility,  developing methods of  prediction,  control,  and
understanding for inherently partial knowledge. Empirical computer
science  should, like physics, focus on prediction and control  in
partially   specified  interactive  modeled  worlds,  since   this
provides  greater  modeling  power  than  completely  formalizable
algorithmic models.

In  showing that the integers were not formalizable by first-order
logic,  Gödel  showed  that  Russell  and  Hilbert's  attempts  to
formalize mathematics could not succeed. These insights also  open
the   door  to  showing  the  limitations  of  formalization   for
computing. The idea of incompleteness, introduced by Gödel to show
that  the natural numbers are not reducible to first-order  logic,
may  be  used  also  to  show  the irreducibility  of  interaction
machines  and more generally of empirical systems whose validation
depends   on   interaction  with  or  observation  of   autonomous
environments. Turing machines lose their statues as  the  natural,
intuitive,  most  powerful computing mechanism  but  retain  their
status  as the most powerful mechanism having a sound and complete
behavior  specification. **These limitations of logic  imply  that
FORMAL CORRECTNESS PROOFS HAVE A LIMITED ROLE AS EVIDENCE FOR  THE
CORRECTNESS  OF  INTERACTIVE  SYSTEMS**.  Hobbes'  assertion  that
"reasoning is but reckoning" remains true since logic is a form of
computing,  but  the  converse assertion that  "reckoning  is  but
reasoning"  is  false since not all computing can  be  reduced  to
logic.

**PROOFS  OF  CORRECTNESS FOR ALL POSSIBLE  INTERACTIONS  ARE  not
merely hard but IMPOSSIBLE FOR SOFTWARE SYSTEMS BECAUSE THE SET OF
ALL  POSSIBLE  INTERACTIONS CANNOT BE SPECIFIED. Testing  provides
the  primary  evidence  for correctness and  other  evidence  like
result  checking  is  needed to check  that  the  result  actually
produced  is  adequate. Even partial result checking, like  parity
checking,  can  greatly increase confidence in  a  result.  Formal
incorporation  of on-line result checking into critical  computing
processes  reinforces  off-line evidence  of  testing  with  post-
execution  evidence that the actual answer is correct. The  nature
of  evidence for the adequacy of computations, the relation  among
different kinds of evidence, and THE LIMITATIONS OF FORMAL METHODS
AND  PROOF  in  providing such evidence ARE IMPORTANT  FUNDAMENTAL
QUESTIONS.**

==================================================================

1)   Are these statements acceptable ("true")? (I don't believe to
   have an adequate mathematical preparation to be able to object,
   but the reasoning, according to me, seems to be correct).
2)   If  the answer is "yes", which will be the role of the proofs
   of  correctness  in  Tunes?  Will  be  limited  to  the  purely
   algorithmic part?  And which will be the importance of the non-
   interactive part (algorithms)? (Wegner defends the central role
   of  interective system in computer science).

-- 
Massimo Dentico