Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?
- To: "coq-club at inria.fr" <coq-club at inria.fr>
- Subject: Re: [isabelle] [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?
- From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein at data61.csiro.au>
- Date: Mon, 18 May 2020 00:54:50 +0000
- Accept-language: en-AU, en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=data61.csiro.au; dmarc=pass action=none header.from=data61.csiro.au; dkim=pass header.d=data61.csiro.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=Gri8zkJKAKn3PAvoH9D9i2wFUJvevbDGAjZ7f9huE9o=; b=bSg+NOLRdbMn35/RMp6HQzBUE1Hk79O8nb23D72iPVML1AlD/8dUgdWa3yXldB70eXSYZtTE+k5sVXBGj5xPjFksGwA/+T9qqDcjFsYtgTFif7jvDbiz2sGo4hZB+tzuHyMHzXSw+CCW6qHO+V1wS5At5EQO1fEZBFLpYE/hai8M+3eQzVsnMngd3gUrqJ3dN0ZjdNpZtLZZicP24owiblGiT4xi+NDcqU4lNdiNLm/8i/7NiWMJCvZwD69TxD57b8ZV5I/PURxpaotKXkXWQPO9HMO/5+hdNCcdQPd86k8VlNW/vCKjmLZyfTnw/k+D6/lMnki7CjkOU9yUgi5AqA==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=VNU8d8hMfgj6+IOdOkqRfWk8eApJ/FQBSHazatTbAi5N8YDoKC48BLV7uvC1SJczCXEJ6t5Ch8rHzuy1+IniYATxYLMBu8vftNFvhxdP+0uRdtYdsHsGm3z1rwdKE2r1+U6AGa9l2EYPvR+rb58ywxJsGq7KKqAgnv6eD4WJ8libNC1TI+Gkm/ZdkF9D16B/UvsthAjnpGDagKlBxtWDnSxLvOnCWF1+V0fBU/0CD2zSZWiU1GMymmtaclbi60CiQ9qhSziGoDkfRUDzlStM4V/luIu8b6Y45/4OjexS1C43loayhffX5oAEdEznaH3PvWhujYt1gTdH+SM3GAATAQ==
- Authentication-results: inria.fr; dkim=none (message not signed) header.d=none; inria.fr; dmarc=none action=none header.from=data61.csiro.au;
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <CAP-V6gnsuOMrYGx4+nV53CQocVHR+4BCmY8ifPU07xOOTeVwUw@mail.gmail.com>
- Ironport-phdr: 9a23:wYf9PBMfhh4woEW0xScl6mtXPHoupqn0MwgJ65Eul7NJdOG58o//OFDEvKw93l7PR4TSrfxe2KLasKHlDGoH55vJ8HUPa4dFWBJNj8IK1xchD8iIBQyeTrbqYiU2Ed4EWApj+He2YklTAsf3IVPI8TW+6DcIEUD5Mgx4bu3+Bo/ViZGx0Oa/s53eaglFnnyze7R3eRm/sQyP748dmop4LeA410jE
- Ironport-sdr: 3qTtcxMqeHP/RR5X2OnuL1y7D1Be2orFySU8S4UsiDGrZJFA4/IrnbV7x/K1Q6xIC/8QYN0/TW +ohOe7WfzUTg==
- References: <CAP-V6gnsuOMrYGx4+nV53CQocVHR+4BCmY8ifPU07xOOTeVwUw@mail.gmail.com>
- Thread-index: AQHWLKUEHmnFAm+fJEG8LmUdmL5TbKitBJKA
- Thread-topic: [Coq-Club] In a world of perfect interoperability between proof assistants, what tools would you combine?
> On 18 May 2020, at 07:42, Talia Ringer <tringer at cs.washington.edu> 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?
CompCert and seL4 would certainly be an attractive combination, because translation validation as we do now in seL4 is a proof every time, whereas CompCert has a once-and-for-all theorem (or at least once that is usable as such).
Assuming HOL4 is also in the mix, which at least for Isabelle it is getting closer and closer to, running CakeML programs on top of that combination would get us a lot closer to end-to-end verified systems. Interoperability with the Verified Software Tool Chain on top of ComCert programs even more.
One is allowed to dream, right? ;-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and