[isabelle] Fwd: Re: A PROBLEM THAT I CAN ALREADY SEE
-------- Videresendt melding --------
Emne: Re: A PROBLEM THAT I CAN ALREADY SEE
Dato: Sat, 5 Dec 2015 21:55:27 +0100
Fra: John Thingstad <jpthing at online.no>
Til: David Blubaugh <davidblubaugh2000 at yahoo.com>
Den 05. des. 2015 19:31, skrev David Blubaugh:
Though it is true that we all dream of creating the best possible
software this goal doesn't always meet real world demands. I suggest you
Thank you so very much for your reply. I however do believe that
formal methods are always worth the cost. This notion of lets create
defective source code and software to throw it out the door to the
market will eventually cost companies in the long run.
For example, it is a simple fact Sandip that you can create good
formally proved software now or you can create defective
near-worthless software now and go through the extensive debugging and
software upgrade cycles in the future. The choice is yours....
That brings me to one question to you Sandip. Why not use the
"correct-by-construction" method ??? That method, I know, would be as
close to perfect as possible to achieving the best of both worlds of
formal methods with rapid software development...
Would the "correct-by-construction" by applicable within ACL2 ?? I
believe it would be.....
What are your thoughts ???
Oh by the way the research work of yours I was referring to was the
manuscript entitled "Scalable Techniques for Formal Verification". I
was truly amazed and impressed with this manuscript....
Also testing is a real alternative to proving and one many software
companies are using today.
For proving to be as unproblematic as testing you need for it to be
easier. Observe the following:
1. Modern languages like Haskell are declarative. So writing a proof is
pointless. Your program IS the specification.
2. So it becomes more like testing. You write assumptions about your
specification and prove that they hold.
Modern proof systems are limited by their knowledge of their domain. A
language that can prove assumptions effortlessly needs to know topology,
algebra and category theory. Only by creating a mathematically sound
type system in this matter can you make a statement and let the computer
access it's validity without requiring you to add a large amount of
In Isabelle it is usual to see 5 lemmas to each proof. Each lemma just
states something that is obvious to anyone to knows maths.
I am working on a language I have chosen to call Formula which tries to
encompass these goals. Whether I succeed or not remains to be seen. In a
world increasingly into parallel computation and distributed processing
traditional testing is becoming increasingly difficult. Proof rather
than testing avoids many of the problems of scaling a algorithm over
Just some thoughts.
This archive was generated by a fusion of
Pipermail (Mailman edition) and