[bitc-dev] BitC prover strategy

[Jonathan S. Shapiro]

I have been pondering a prover strategy question. I'ld like to open it
for discussion.

We have been heading in the direction of building a prover, on the
grounds that Isabelle is insufficiently automated. It has occurred to me
that this may be short-sighted. Here is an alternative.

Suppose that instead of building a new prover, we create Isabelle/BitC.
This is similar to Isabelle/ISAR, except that the language of theory
expression is BitC. There is certainly no reason that we would need to
restrict ourselves to the style of recdef definitions that I can see.

On the topic of automation, we can either develop new tacticals or
modify the term rewriting engine of Isabelle to detect and blacklist
expansion loops.

On the other hand, once we are doing this it will be true that pretty
much the *only* part of Isabelle we will be preserving is the rewriting
engine, which may not be that big a deal.

Reactions?
-- 
Jonathan S. Shapiro <shap at eros-os.org>