[Prev][Next][Index]

Re: A question

> Hi, all! This maybe a naive question. But I have always wondered why
> one shouldn't use a proven powerful verification system such as Nqthm
> (Boyer-Moore theorem prover) for specification of programs. After all
> when you verify a program you have to express the specification of the
> program.  Nqthm has been used sucessfully to verify programs in a
> number of languages. So why not use that? 

     The answer to this question is the same as the answer to the question of
why one shouldn't use a prover powerful programming language such as ... fill
in the name of your favorite language ... for writing programs.  People's
preferences, whether for programming languages or theorem provers, are affected
by many factors: the syntax and semantics of the language, the levels of
abstraction provided, ease of use, learnability, libraries, ...  People can and
do use Nqthm.  But other people also can and do use other provers.

>                                            Why use systems like Larch
> and LP which are specifically geared only to express specifications and
> not verification? 

     You are mistaken in thinking that LP is not geared toward verification.
The various Larch languages (LSL, LCL, ...) are specification languages, but LP
is a general purpose theorem proving environment.  People who use Larch as a
specification language often prefer to use LP rather than Nqthm because there
are tools that translate Larch specifications into input for LP; people who
want to use Nqthm as a prover either must design and implement their own
specification language within Nqthm or implement a translation from Larch (or
some other) specifications into Nqthm.

>                    Of course there are cosmetic differences like one is
> a typed language and the other is not, etc. But I think these can be
> ignored.

     Some would argue that differences in the type system or the logic are much
more than cosmetic.  Others would argue that even cosmetic differences cannot
be ignored, because they can make a big difference in practice.
Reference(s):