[Caml-list] Formal Methods

[Caml-list] Formal Methods

[David McClain]

[-- Attachment #1: Type: text/plain, Size: 765 bytes --]

I have just been reviewing some papers by Greg Chaitin on Algorithmic 
Complexity Theory, in which he boldly states that

"Similarly, proving correctness of software using formal methods is 
hopeless. Debugging is done experimentally, by trial and error. And 
cautious managers insist on running a new system in parallel with the 
old one until they believe that the new system works."

from

http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html

He goes to great lengths to discuss the halting problem and its 
implications for proving correctness of algorithms.

I wonder, as a non-specialist in this area, how the goals of FPL 
squares with this result?

David McClain
Senior Corporate Scientist
Avisere, Inc.

david.mcclain@avisere.com
+1.520.390.7738 (USA)


[-- Attachment #2: Type: text/enriched, Size: 852 bytes --]

I have just been reviewing some papers by Greg Chaitin on Algorithmic
Complexity Theory, in which he boldly states that 


"<fontfamily><param>Times</param><bigger><bigger>Similarly, proving
correctness of software using formal methods is hopeless. Debugging is
done experimentally, by trial and error. And cautious managers insist
on running a new system in parallel with the old one until they
believe that the new system works."


from 


http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html


He goes to great lengths to discuss the halting problem and its
implications for proving correctness of algorithms.


I wonder, as a non-specialist in this area, how the goals of FPL
squares with this result?

</bigger></bigger></fontfamily>

David McClain

Senior Corporate Scientist

Avisere, Inc.


david.mcclain@avisere.com

+1.520.390.7738 (USA)

RE: [Caml-list] Formal Methods

[Jacques Carette]

[-- Attachment #1: Type: text/plain, Size: 2103 bytes --]

The same 'problem' occurs in symbolic computation: the zero-equivalence
problem for constants is well-known to be undecidable.  However, in
practice, constants that appear in real problems (ie ones that occur from
physical models) are very easy to prove non-zero.  The constants that are
difficult to handle tend to arise in idealized settings.
 
Now that I have started also using Formal Methods for proving my code
correct, I have encountered the same thing: most meaningful programs can be
proven correct (given the right tools), but I can also construct short silly
programs which none of the standard tools handle.
 
I also see an analogy with type systems such as Ocaml's: in theory, type
inference is exponential, while in practice it is very fast.  This is
because the worst cases are very degenerate, and do not tend to occur in
common / meaningful programs.
 
Consider the above as a meta-observation based on my experience, first as
Sr. Architect at Maplesoft, now as a researcher applying formal methods to
computer algebra.
 
Jacques
 

-----Original Message-----
From: owner-caml-list@pauillac.inria.fr
[mailto:owner-caml-list@pauillac.inria.fr] On Behalf Of David McClain
Sent: September 30, 2004 11:51 AM
To: caml-list@inria.fr
Subject: [Caml-list] Formal Methods


I have just been reviewing some papers by Greg Chaitin on Algorithmic
Complexity Theory, in which he boldly states that 

"Similarly, proving correctness of software using formal methods is
hopeless. Debugging is done experimentally, by trial and error. And cautious
managers insist on running a new system in parallel with the old one until
they believe that the new system works."

from 

http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html

He goes to great lengths to discuss the halting problem and its implications
for proving correctness of algorithms.

I wonder, as a non-specialist in this area, how the goals of FPL squares
with this result?

David McClain
Senior Corporate Scientist
Avisere, Inc.

david.mcclain@avisere.com
+1.520.390.7738 (USA)




[-- Attachment #2: Type: text/html, Size: 3766 bytes --]

Re: [Caml-list] Formal Methods

[Jon Harrop]

On Thursday 30 September 2004 18:35, Jacques Carette wrote:
> I also see an analogy with type systems such as Ocaml's: in theory, type
> inference is exponential, while in practice it is very fast.

I'd contest the "very fast".

When writing an API for my vector graphics engine, I wrote a lot of generic 
HOFs. The time taken to compile increased by a factor of ten. This prompted 
me to split my sources into separate compilation units to speed partial 
recompilations.

I believe the slow compile times are due to the complicated types involved 
(often half a page in the .mli) although the functions themselves are often 
very simple. So I think the time taken for compilers to deal with types can 
be very significant and can influence programming. So I don't think type 
handling is not always "very fast" in practice.

Cheers,
Jon.

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

RE: [Caml-list] Formal Methods

[Thomas Fischbacher]

On Thu, 30 Sep 2004, Jacques Carette wrote:

> I also see an analogy with type systems such as Ocaml's: in theory, type
> inference is exponential, while in practice it is very fast.  This is
> because the worst cases are very degenerate, and do not tend to occur in
> common / meaningful programs.

Well, I this is quite different from what I experience if I use a (perl) 
code-generator which spits out ocaml code.

I don't know if this is still a problem, but I already encountered severe 
difficulties when trying to compile a fixed constant definition of an 
array (length ~380 000) of arrays (length ~10) of strings (length ~4).

-- 
regards,               tf@cip.physik.uni-muenchen.de              (o_
 Thomas Fischbacher -  http://www.cip.physik.uni-muenchen.de/~tf  //\
(lambda (n) ((lambda (p q r) (p p q r)) (lambda (g x y)           V_/_
(if (= x 0) y (g g (- x 1) (* x y)))) n 1))                  (Debian GNU)

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Formal Methods

[Achim Blumensath]

On Fri, Oct 01, 2004 at 10:24:15AM +0200, Thomas Fischbacher wrote:
> On Thu, 30 Sep 2004, Jacques Carette wrote:
> > I also see an analogy with type systems such as Ocaml's: in theory, type
> > inference is exponential, while in practice it is very fast.  This is
> > because the worst cases are very degenerate, and do not tend to occur in
> > common / meaningful programs.
> 
> Well, I this is quite different from what I experience if I use a (perl) 
> code-generator which spits out ocaml code.
> 
> I don't know if this is still a problem, but I already encountered severe 
> difficulties when trying to compile a fixed constant definition of an 
> array (length ~380 000) of arrays (length ~10) of strings (length ~4).

I don't think this is related to the type system of OCaml. It seems to
be just an inefficient implementation: the part of the compiler dealing
with arrays is apparently not tail-recursive (see feature wish 2306 in
the bug database).

Achim
-- 
________________________________________________________________________
                                                              | \_____/ |
   Achim Blumensath                                          \O/ \___/\ |
   LaBRI / Bordeaux                                          =o=  \ /\ \|
   www-mgi.informatik.rwth-aachen.de/~blume                  /"\   o----|
____________________________________________________________________\___|

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

[Off-topic] Re: [Caml-list] Formal Methods

[David MENTRE]

Hello,

David McClain <David.McClain@Avisere.com> writes:

> I wonder, as a non-specialist in this area, how the goals of FPL squares
> with this result?

As a "real world" example, AMD is proving the FPU of its processors with
ACL2, which is a functional subset of Common Lisp. However, the FPU
themselves are not written in a functionnal language but in hardware
language translated in Register Transfer Language (RTL). A translator is
used for RTL->ACL2 translation and then proving.

  http://www.cs.utexas.edu/users/moore/acl2/


If I remember correctly, Coq has been used in Cristal research team to
prove part(?) of OCaml type system.

Yours,
david

PS: I'm neither a specialist in this area.
-- 
 David MENTRÉ <dmentre@linux-france.org>

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Formal Methods

[Jean-Christophe Filliatre]

David McClain writes:
 > I have just been reviewing some papers by Greg Chaitin on Algorithmic 
 > Complexity Theory, in which he boldly states that
 > 
 > "Similarly, proving correctness of software using formal methods is 
 > hopeless. Debugging is done experimentally, by trial and error. And 
 > cautious managers insist on running a new system in parallel with the 
 > old one until they believe that the new system works."
 > 
 > I wonder, as a non-specialist in this area, how the goals of FPL 
 > squares with this result?

Proving a purely functional code  is definitely easier than proving an
imperative one;  you'll find several  projects to verify  Haskell code
(such  as OGI's  Programatica) and  many JFP  Functional  Pearls where
equational  reasoning   is  applied  to  Haskell  code   to  prove  it
correct. You  can also use  the logic of  a proof assistant  to encode
directly  purely  functional  programs  and prove  them  correct  (for
instance the OCaml  library Set has been proved  correct using the Coq
proof assistant; and a small bug was found during the formal proof, so
you can't say ``using formal methods is hopeless'').

The  real   difficulties  in  proving  functional   code  appear  when
side-effects are mixed with  powerful features such as polymorphism or
higher-order.   Then it becomes  very hard  to reason  about programs.
Actually,  we  don't  even  have  a specification  language  to  write
programs  properties to  be  proved.  There is  a  nice challenge  for
research here.

(Regarding more  traditional imperative programming  languages, I must
disagree with  Chaitin's statement: formal  methods are more  and more
applied  to critical  software.   But it  requires  a lot  of work  to
formally verify  a few  lines of code,  so it  only applies to  a very
small number of highly critical softwares.)

-- 
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Formal Methods

[Tom]

An example of formal methods applied to traditional imperative
programming is the proof of a full copying garbage collector, using
separation logic, by Birkedal et al:

http://www.itu.dk/people/noah/papers/gc-popl.ps

Jean-Christophe Filliatre writes:
 > 
 > David McClain writes:
 >  > I have just been reviewing some papers by Greg Chaitin on Algorithmic 
 >  > Complexity Theory, in which he boldly states that
 >  > 
 >  > "Similarly, proving correctness of software using formal methods is 
 >  > hopeless. Debugging is done experimentally, by trial and error. And 
 >  > cautious managers insist on running a new system in parallel with the 
 >  > old one until they believe that the new system works."
 >  > 
 >  > I wonder, as a non-specialist in this area, how the goals of FPL 
 >  > squares with this result?
 > 
 > Proving a purely functional code  is definitely easier than proving an
 > imperative one;  you'll find several  projects to verify  Haskell code
 > (such  as OGI's  Programatica) and  many JFP  Functional  Pearls where
 > equational  reasoning   is  applied  to  Haskell  code   to  prove  it
 > correct. You  can also use  the logic of  a proof assistant  to encode
 > directly  purely  functional  programs  and prove  them  correct  (for
 > instance the OCaml  library Set has been proved  correct using the Coq
 > proof assistant; and a small bug was found during the formal proof, so
 > you can't say ``using formal methods is hopeless'').
 > 
 > The  real   difficulties  in  proving  functional   code  appear  when
 > side-effects are mixed with  powerful features such as polymorphism or
 > higher-order.   Then it becomes  very hard  to reason  about programs.
 > Actually,  we  don't  even  have  a specification  language  to  write
 > programs  properties to  be  proved.  There is  a  nice challenge  for
 > research here.
 > 
 > (Regarding more  traditional imperative programming  languages, I must
 > disagree with  Chaitin's statement: formal  methods are more  and more
 > applied  to critical  software.   But it  requires  a lot  of work  to
 > formally verify  a few  lines of code,  so it  only applies to  a very
 > small number of highly critical softwares.)
 > 
 > -- 
 > Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)
 > 
 > -------------------
 > To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
 > Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
 > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Formal Methods

[Martin Berger]

> The  real   difficulties  in  proving  functional   code  appear  when
> side-effects are mixed with  powerful features such as polymorphism or
> higher-order.   Then it becomes  very hard  to reason  about programs.
> Actually,  we  don't  even  have  a specification  language  to  write
> programs  properties to  be  proved.  There is  a  nice challenge  for
> research here.

this has changed recently. please consider

   http://www.doc.ic.ac.uk/~yoshida/paper/PA.ps
   http://www.doc.ic.ac.uk/~yoshida/paper/polyrec.ps
   http://www.doc.ic.ac.uk/~yoshida/paper/icfp04.ps

more along those lines is in the pipeline.

martin

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Formal Methods

[Hendrik Tews]

David McClain <David.McClain@Avisere.com> writes:

   I have just been reviewing some papers by Greg Chaitin on Algorithmic
   Complexity Theory, in which he boldly states that
   
   "Similarly, proving correctness of software using formal methods is
   hopeless. 

This is just nonsense. You can prove the correctness of any piece
of software (provided it is correct). Its only some orders of
magnitute more expensive than developing the same software,
therefore proving correctness is seldom attempted in practice. 

Further the halting problem is just not relevant here. It only
means that you can not hope for a fully automatic procedure.
However, every decent programmer knows why his while loops
terminate. So you just go and ask him and use his answer in your
correctness proof. In general, software verification is not
difficult, it is complex. 

   I wonder, as a non-specialist in this area, how the goals of FPL
   squares with this result?
   
If you have a well-typed programm for a language with a strong
type system you can use a simpler semantics. Thus verification
becomes cheaper. Now, if you have a side-effect free language,
like Haskell, it becomes even more simpler and cheaper. However,
nowadays a semantics exists even for quite dirty languages like
Java, C or C++. You are not bound to functional programming if
you want to use formal methods. Goto statements, pointer
arithmetic and even type casts are not a problem if you use the
right technology.

Bye,

Hendrik Tews 

(I am working in the VFiasco project that attempts to verify
properties of the Fiasco micro-kernel written in C++. 
Checkout http://os.inf.tu-dresden.de/vfiasco/) 

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

Re: [Caml-list] Formal Methods

[Martin Berger]

>    "Similarly, proving correctness of software using formal methods is
>    hopeless. 
> 
> This is just nonsense. You can prove the correctness of any piece
> of software (provided it is correct). Its only some orders of
> magnitute more expensive than developing the same software,
> therefore proving correctness is seldom attempted in practice. 

it is a bit more complicated than that. it seems to be the case, and
maybe that's what chaitin is getting at, that the more complicated
the program under verification and the more complicated the property
to be established, the more that verification is like writing a program.
but then the question "is the specification correct?" becomes as hard
as, or identical with "has the program that property?". so in the limit
there seems to be a real problem in that we can trust  verification
only in as much as we can trust programming.

BUT, and that's a very big "but", for many properties that happen to be
of human interest, such as the absence of buffer-overflow errors, or
the fact that a given program terminates, verification is often fairly
easy to do and specification of the relevant property
is easy. so easy in fact sometimes that it can be automatised. Sriram
Rajamani for example, http://research.microsoft.com/~sriram/ has
recently come up with some surprisingly powerful automatic verification
tools.

in summary, it seems that chaitin is right, but for properties and
programs as simple as those humans care about, formal verification
tends to be possible.

martin

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners

RE: [Caml-list] Formal Methods

[Harrison, John R]

[-- Attachment #1: Type: text/plain, Size: 2009 bytes --]

When he says that "theorem proving algorithms do not work [...] they
only prove trivial theorems",
he may just be out of date, or he may only be talking about completely
automatic provers. (Even
then his claim is a bit questionable: what about the Robbins Conjecture
etc.?)
 
I didn't notice anything about the relevance of the halting problem in
that page, so maybe it's
somewhere else. Anyway, it's clearly not relevant to proving the
correctness of typical real-world
algorithms, whatever he may or may not say.
 
His general dismissive attitude to formal methods is not uncommon. And
it's prefectly reasonable
to point out that modern computer systems can be so complex and
ill-defined that they are hardly
amenable to formal treatment. But a more balanced view would acknowledge
the significant
success of formal methods in certain niches, and their role in trying to
check that very unmastered
complexity. 
 
John.

	-----Original Message-----
	From: owner-caml-list@pauillac.inria.fr
[mailto:owner-caml-list@pauillac.inria.fr] On Behalf Of David McClain
	Sent: Thursday, September 30, 2004 8:51 AM
	To: caml-list@inria.fr
	Subject: [Caml-list] Formal Methods
	
	
	I have just been reviewing some papers by Greg Chaitin on
Algorithmic Complexity Theory, in which he boldly states that 

	"Similarly, proving correctness of software using formal methods
is hopeless. Debugging is done experimentally, by trial and error. And
cautious managers insist on running a new system in parallel with the
old one until they believe that the new system works." 

	from 

	http://www.cs.auckland.ac.nz/CDMTCS/chaitin/omega.html 

	He goes to great lengths to discuss the halting problem and its
implications for proving correctness of algorithms. 

	I wonder, as a non-specialist in this area, how the goals of FPL
squares with this result? 
	David McClain 
	Senior Corporate Scientist 
	Avisere, Inc. 

	david.mcclain@avisere.com 
	+1.520.390.7738 (USA) 



[-- Attachment #2: Type: text/html, Size: 4596 bytes --]