But we will have to also support 4.10.2 / 4.12 for M1 folks (including, soon, me); luckily, I don't (yet) see us using Alectryon locally, but this will require some CI effort on testing an extra configuration.
well, I would argue that testing with different OCaml versions is good anyway, similar to using both coq_makefile for dev and Dune in CI
Generally, libraries and plugins absolutely need to, "applications" can be more closed world.
(at least that's the Haskell experience)
I guess the main concern is bugs in plugins that are version-dependent, so in principle we'd have to redo the full CI on both versions?
when you develop open source stuff to be consumed by "everyone" for purposes you haven't thought of, that's a bit different from "applications" I think. So sure, if you have very specific "customers" you can do the whole thing with lock files...
I'd count that as "libraries"
While eg the seL4 proofs are closer to "applications"
Even if it's true that they could have more clients than a typical application, in principle.
Also you're entitled to care more for open-source libraries than proprietary applications!
in a world hopefully soon to arrive ("open science"), researchers will be forced by their grants to not needlessly lock down their artifacts and go full library, even for narrow formalizations
I’m a fan of open science, but the Coq community _might_ like to enable verifying industrial software, even if that’s closed-source. I guess BSD-like licenses signal openness to that :-)
anyway, sorry for dragging us into such a wild OT!
I broke off the topic a bit to fix that. I guess we can move to Coq users also.
This topic was moved here from #Coq Platform devs & users > Testing with multiple OCaml versions by Karl Palmskog
@Paolo Giarrusso at the risk of igniting flames, I find it hard to understand how industrial verification works out when everything is kept under wraps. If people are not allowed to actually build/see specs & proofs, you will be forced to trust company and possibly auditors, as usual
I’ll get to that in a sec… on the “versions” thread: on more concrete questions, how often do proofs break on a specific OCaml version? I guess it’s mostly “build fails on some step”.
at the very least it would make sense if some core specs & library is made public and vetted, and then a customer might be allowed to reduce their TCB to that
I don’t disagree!
the main failures I see with OCaml are when your proofs and specs depend on OCaml plugins, and with the build system and possibly extracted code and so on. And
TCB-wise, all I _can_ say is that our C++ axioms are already public, even if under the license you don’t like
and as a rule I only try to say things that are already public — for instance, many of us come from academia so we’re aware of those kinds of questions
well, is there a public axiom validation? E.g., empirical evidence this actually capture what C++ compilers are doing, etc.
not exactly the best analogy, but I thought the validation of the ELF formalization was nice: https://www.cl.cam.ac.uk/~pes20/rems/papers/oopsla-elf-linking-2016.pdf
I’m pretty confident you would not yet be satisfied
not by the public material, at least — and I’m not going to make claims about any private material, because I can’t, and because you wouldn’t (and shouldn’t) believe me :-)
OK, sure, I was just asking about "does there exist something like X that is public"
I can say that semantics is a work-in-progress, and I tried to make sure the claims are clear, and they’re probably not prominent enough yet.
(we’re currently polishing these docs up)
is the scope of the axioms functional/behavioral only or do you consider non-functional properties (information flow, memory space, ...)?
thankfully, our internal setup allows us to progress on verification without a finished C++ semantics…
I’d say functional-only
one point that was made to me recently by a cryptocurrency insider: the cryptocurrency industry uses formal verification primarily for conflict resolution, not certainty down to bit level. So there at least, the incentives align a bit more with "open science".
anyway, I’m not yet going to argue this semantics is “correct” yet; count this as a “release early, release often” version.
“conflict resolution”? conflicts between bits or humans?
conflicts between humans about adopting protocols and the like ("most verified wins")
well, going from a 2000-page(?) language spec in English down to hundreds/thousands of Coq lines seems worthwhile
also fun to see all the formal verification shilling, all the Hedera proponents are seemingly perpetually excited about Karl Crary's Coq formalization of a protocol Hedera (supposedly) uses (https://www.cs.cmu.edu/~crary/papers/2021/hashgraph.pdf)
Paolo Giarrusso said:
how often do proofs break on a specific OCaml version? I guess it’s mostly “build fails on some step”.
I have a piece of Coq code that inexplicably breaks with OCaml >= 4.10. I've been meaning to open a bug report for ages, but wanted to find a MWE, and so far that's proved too time consuming and annoying. I guess I could feed it to the minimizer...
Non-minimal bug reports are IMHO better than nothing, @Ana de Almeida Borges
Last updated: Sep 26 2023 at 13:01 UTC