Email Gateway (Aug 23 2022 at 09:03): Email Gateway (Aug 23 2022 at 09:03):From: Abhishek Anand <abhishek.anand.iitg@gmail.com>
I'd like to understand why such a tool/setup doesn't exist.
Because of technical difficulties?
Because such projects won't be cool enough to publish in "top conferences"
and please the career gods?
I very vaguely remember hearing about attempts to make such tools, about
3-5 years ago. I'd love to hear their experience.
Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/
Email Gateway (Aug 23 2022 at 09:10):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
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? ;-)
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 09:10):From: Talia Ringer <tringer@cs.washington.edu>
Just for clarity, I said "tools" which was a bit ambiguous, but I meant
more along the lines of what Gerwin wrote. Appreciate the useful thoughts
from all regardless :)
Email Gateway (Aug 23 2022 at 09:10):From: roux cody <cody.roux@gmail.com>
Isabelle seems to really shine in proof automation, but obviously it
doesn't hold much of a candle to automated theorem provers like Vampire,
Z3, Minisat, ACL2 (to a certain extent) etc.
Coq has the remarkable advantage that a lot of it's extra structure, type
classes, proof witnesses, computational reflection, come for free within
the kernel (with the notable exception of modules). Of course this kernel
is quite complex, almost the opposite of HOL-light's, which is remarkably
trustworthy.
Almost every widely used tool has unique libraries and tactics which are
found in no others, of course.
It's hard to tell which of these differences are intrinsic tensions of the
tool designs and which are incidental. Contrary to similar debates about
programing languages, however, it seems that every one of these can be
embedded in some, reasonably trustworthy, super-logic, roughly on par of
ZFC + largish cardinal axiom. At the cost of some severe foundational
debates though, I guess.
Logics which are really useful and popular right now are linear, modal and
seperation logics, which have to be embedded into such a system along with
a proof of soundness if you want the same level of trust. This is usually
extremely tedious, at least given my limited experience, both WRT notations
and proof conveniences. I've seen several examples of systems originally
designed as a deep embedding which were then turned into standalone tools
because of this tension (CertiCrypt springs to mind).
I'm not sure this tension can be resolved, since there is no common ground
in this case (to my knowledge). Twelf might make such a claim as a unifier,
but it is a very thin veneer over the astronomical amount of work required
to make the logic even remotely usable. There's a reason why in 99% of
cases the word "Isabelle" is followed by "/HOL". Logical frameworks have so
far not lived up to their promise.
As is usually the case in the PL world, usable languages are often usable
because of the quality of the libraries, and their ease of installation.
This is largely a language specific effort, unfortunately. This makes me
something of a pessimist, as in most domains, but I guess someone's got to
occupy that quadrant.
Thanks for the opportunity to rant,
Cody
Email Gateway (Aug 23 2022 at 09:11):From: Mark Wassell <mpwassell@gmail.com>
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
Last updated: Apr 24 2024 at 20:16 UTC