The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

+1

On Tue, May 19, 2020 at 9:33 AM Mark Wassell <mpwassell AT gmail.com> wrote:

> Most notably on the existing work that can span proof assistants, I think of the SAIL project for hardware architectures which has an Isabelle

> (or HOL?) backend and a Coq backend (though it is a bit behind the other one).

As an aside: From the same stable as Sail there is also Lem (https://github.com/rems-project/lem) which follows the same idea of exporting to multiple backends including multiple theorem provers (Isabelle/HOL, HOL4 and Coq). Whilst targeted at "lightweight executable mathematics, for writing, managing, and publishing large-scale portable semantic" this is after all what a lot of us use theorem provers for.

Cheers

Mark

On Tue, 19 May 2020 at 14:23, Gregory Malecha <gregory AT bedrocksystems.com> wrote:

For me, the most useful things to be able to share would be formalizations of standards. These tend to be "boring" but necessary for building systems that run in real life. There is a lot of work in this and some of it is even portable due to its development.

Most notably on the existing work that can span proof assistants, I think of the SAIL project for hardware architectures which has an Isabelle (or HOL?) backend and a Coq backend (though it is a bit behind the other one).

As you move up the stack, however, things separate. I'm more familiar with the work in Coq, but many projects have already been listed. But one thing that I didn't notice are non-CPU hardware models. E.g. devices like interrupt controllers, ethernet cards, etc. Slightly more abstract would be things like the VirtIO specification which is generally fairly common across architectures and different software stacks.

Higher up the toolchain most people have already noted. Language standards are the things that we think about the most, CakeML, CompCert C, etc, but there are other ones as well. Robbert Krebber's thesis has a formalization of the C standard that attempts to follow the standard more closely than CompCert C, we are working on a model and program logic for the C++ standard, I'm aware of work on the Ethereum virtual machine in HOL as well. The work at UPenn on the semantics of LLVM is also very notable in this context.

It would be amazing to try to share automation-style tools across the different provers, but I think that is a more ambitious goal (one I'm not certain is entirely possible due to the vastly different styles). However, I think that it should be completely reasonable to write models in a slightly stylized way to achieve portability across theories.

On Mon, May 18, 2020 at 9:09 AM Peter Lammich <lammich AT in.tum.de> wrote:

Hi

I would like to see Compcert, at least its backend (IR, optimizations,
machine code generation), being usable from Isabelle.
Then I could probably retarget my Refinement Framework to use Compcert-
IR as a backend, closing the gap from very high-level specifications to
machine code. Similar for CakeML (Currently, the Refinement Framework
targets LLVM or SML).

--
  Peter



On Sun, 2020-05-17 at 16:42 -0700, Talia Ringer wrote:
> Say we one day are able to just take things from Isabelle/HOL and use
> them
> with Coq developments with no additional effort, or similarly in the
> opposite direction, or similarly for any other pair of proof
> assistants.
> Say we would get strong guarantees about these combined verified
> systems.
> Just humor this for a second.
>
> In such a world, what systems would you want to combine, and why?
>
> Talia

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING