🚀 go-pugleaf

In article <935@scaup.cl.cam.ac.uk> scc@cl.cam.ac.uk (Stephen Crawley) writes:


   Bill Wolfe replies:

   > Finally, formal verification is a
   > major goal of the software engineering community, and Ada was designed
   > to support it to as great an extent as possible.  For example, the
   > use of the termination model of exception handling was (at least in
   > part) motivated by formal verification considerations. 

   Excuse me while I laugh ...

   Verifying ADA 83 is a fundamentally intractible problem for any number
   of reasons.  I don't believe anyone has even managed to formally define
   the semantics of ADA 83!  Maybe some members of the ADA design team did 
   have verification in their minds ... but others didn't, and the others
   won the day.


compare this situation to that of scheme where the formal semantics of
the language _have_ been defined, and they are concise enough to fit on
a couple of pages.  in fact, they are so simple and straightforward
that the formal semantics can be used in an undergraduate computer
science class.

even more interesting, these formal semantics were automatically
derived from a running scheme program which provides an executable
model of the semantics.  this allows much simpler testing of the
semantics than just writing down the equations and having people stare
at them.



--
ted@nmsu.edu
			remember, when extensions and subsets are outlawed,
			only outlaws will have extensions or subsets