Email Gateway (Aug 22 2022 at 12:07): Email Gateway (Aug 22 2022 at 12:07):From: John Thingstad <jpthing@online.no>
-------- Videresendt melding --------
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:
Modern languages like Haskell are declarative. So writing a proof is
pointless. Your program IS the specification.
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
Last updated: Nov 21 2024 at 12:39 UTC