Subject: Re: Accellera: Branching vs. Linear Time
From: Moshe Vardi (vardi@cs.rice.edu)
Date: Mon Jul 09 2001 - 23:48:11 PDT
>
> ed> I think the point you make in the second part of your message is
> ed> an important one. In addition to deciding on what language to use,
> ed> we really need to decide on how compositional reasoning and
> ed> refinement should be done as well.
>
> it is an important point, but it occurs to me it might be furitful to
> start from a slightly different question: to what degree are these
> concerns separable?
>
> we *could* seek a "logical framework" (i use the term tentatively in
> the extreme!) for conducting the sort of meta reasoning
>
> M || M' |= p iff M |= f(M') -> p
>
> that is commonly used, such that the proof (p holds) is fully formal.
> but wouldn't that be monadic second order logic (making issues of mere
> syntax slightly irrelevant)?
Which is why you need the full power of \omega-regularity,
but syntax is hardly irrelevant to users.
>
> at the other end we might conclude something like this: since in any
> case in order to do a mechanical proof we'll need deep abstractions in
> order to get "M" small & simple enough, and these may be more or less
> formally applied, there's little point in a logical framework since
> our proofs will be at best "informal." so use any compositional
> reasoning methodology you find that works.
>
so much for "formal verification".
Moshe
This archive was generated by hypermail 2b28 : Mon Jul 09 2001 - 23:48:47 PDT