Mailing list for all users of the OCaml language and system.
 help / color / mirror / Atom feed
From: David McClain <David.McClain@Avisere.com>
To: caml-list@inria.fr
Subject: [Caml-list] Formal Methods
Date: Thu, 30 Sep 2004 08:51:25 -0700	[thread overview]
Message-ID: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> (raw)

[-- 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)



             reply	other threads:[~2004-09-30 15:51 UTC|newest]

Thread overview: 12+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2004-09-30 15:51 David McClain [this message]
2004-09-30 17:35 ` Jacques Carette
2004-09-30 18:42   ` Jon Harrop
2004-10-01  8:24   ` Thomas Fischbacher
2004-10-01  9:01     ` Achim Blumensath
2004-09-30 17:54 ` [Off-topic] " David MENTRE
2004-10-01  7:36 ` Jean-Christophe Filliatre
2004-10-01  7:51   ` Tom
2004-10-01  9:04   ` Martin Berger
2004-10-01  8:30 ` Hendrik Tews
2004-10-01  9:18   ` Martin Berger
2004-09-30 17:19 Harrison, John R

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com \
    --to=david.mcclain@avisere.com \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body. 
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox