🚀 go-pugleaf

David Gudeman says:
[quote]
   ]
   ]Usually not, because the specification is at a higher level and closer
   ]to the way a person thinks than an implementation.

   That is an argument for higher-level programming languages (with
   dynamic typing, for instance), not an argument for adding another
   language (the specification language) to the process of implementing
   software.  If your specification is so great, why not make that your
   programming language?
[end quote]

Because specifications need not be constructive. Consider

    fn sqrt
        is sqrt x pre x >= 0 return y post y * y = x

[This is a piece of HP-SL, a VDM derivative we're working on.] Any suggestions
on how to compile this to code that you'd use in Real Life? Or

    fn invf
        is invf (f, f') == (FORALL x. f' (f x) = x)

which tests two functions to see if one is the inverse of the other? I'm all in
favour of raising the level of programming languages, but the point of a
specification language is to describe the intended behaviour without being
constrained by the details of a language that is perforce intended to manifest
that behaviour on (usually) a sequential machine in (usually) a reasonably
short time.

[Incidentally, the type-checker tells me that the types of those functions are

fn invf : (_A -> _B) -> ((_B -> _A) -> Bool)
fn sqrt : Num -> Num

Just what I wanted. *In this case*, static type-checking is fine.]
--

Regards, Kers.      | "You're better off  not dreaming of  the things to come;
Caravan:            | Dreams  are always ending  far too soon."