[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:
Sandip,

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....

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 read:
https://www.dreamsongs.com/WorseIsBetter.html

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 extra information.

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 multiple processors..

Just some thoughts.

John





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.