Zen and the Art of Formal Specification (was: Re: Zed and the Art of Functional Programming)

On Tuesday 20 March 2007 22:54, Shriram Krishnamurthi wrote[0]:
> > Seriously though, FP and Z seem like a good match from where I sit.
> > Wouldn't you vigorously agree?
>
> I would, quite vigorously.
>
> But your original message was somewhat more provocative.  Setting aside the
> actual theory part of your hilarious conspiracy theory, the condition you
> claimed to be noticing was the "paucity of FP-oriented UML/OCL-like
> notations".  If you admit Z, then you really ought to admit the many other
> formal modeling languages that sit atop theorem provers (UNLESS YOU WANT TO
> ARGUE they don't fit your definition of modeling languages)

I do want to argue precisely that.  As far as I am concerned, the purpose of Z
is to help you strip a problem down to its essence, its "irreducible
complexity" as you call it[1].  In contrast -- to the best of my very limited
knowledge -- the purpose of theorem provers is to prove a program correct.
And you know what they say about that:

  | [...] formal verifications of programs, no matter how obtained,
  | will not play the same key role in the development of computer
  | science and software engineering as proofs do in mathematics.
  | Furthermore the absence of continuity, the inevitability of
  | change, and the complexity of specification of significantly many
  | real programs make the formal verification process difficult to
  | justify and manage.  [...] ease of formal verification should not
  | dominate program language design.

Restated in more pedestrian terms:

  | [...] there is no continuity between the world of FIND and GCD and
  | the world of production software, billing systems that write real
  | bills, scheduling systems that schedule real events, ticketing
  | systems that issue real tickets.

> ... as well as synthesis languages such as Specware.  They are all very
> FP-friendly.  They just happen to traffic in text rather than diagrams,
> unlike the majority of the UML notations.

No beef between me and text traffickers.  Note that I explicitly included OCL
in my sample of OOP-oriented modeling languages.

Even though I dismiss systems that sit atop theorem provers, I am starting to
warm up to ones that sit atop SAT solvers.  Big thanks to Scott McKay for
turning me onto Alloy[2], a wonderful piece of work by Daniel Jackson of the
Jackson clan of formal specification[3]. (Incidentally, a Brit[4].)


But none of this has any bearing on the original observation.  There are a lot
of notations geared specifically towards OOP.  The best you can claim for FP
is that there are many notations that are *friendly* to it, but none that are
custom-tailored for it the way UML is for OOP[5].

Vadim
______________________________________________________________________________
Footnotes

 0. Message-ID: <[email protected]>
    https://lists.csail.mit.edu/pipermail/ll-discuss/2007-March/001370.html

 1. "irreducible complexity"
    Message-ID: <[email protected]>
    https://lists.csail.mit.edu/pipermail/ll-discuss/2007-March/001358.html

 2. Alloy
    http://scholar.google.com/scholar?cluster=2429633968389581994
    http://alloy.mit.edu/

 3. Michael Jackson
    http://www.amazon.com/Software-Requirements-Specifications-ACM-Press/dp/0201877120/

 4. Message-Id: <[email protected]>
    https://lists.csail.mit.edu/pipermail/ll-discuss/2007-March/001337.html

 5. Levine the Genius Tailor
    http://lambda-the-ultimate.org/node/1014#comment-10571