# [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.*