Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?



 > 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*
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.