Paolo Giarrusso (Nov 16 2021 at 14:00): Paolo Giarrusso (Nov 16 2021 at 14:00):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.
Karl Palmskog (Nov 16 2021 at 14:00):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
Paolo Giarrusso (Nov 16 2021 at 14:01):Generally, libraries and plugins absolutely need to, "applications" can be more closed world.
Paolo Giarrusso (Nov 16 2021 at 14:02):(at least that's the Haskell experience)
Paolo Giarrusso (Nov 16 2021 at 14:03):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?
Karl Palmskog (Nov 16 2021 at 14:03):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...
Paolo Giarrusso (Nov 16 2021 at 14:03):I'd count that as "libraries"
Paolo Giarrusso (Nov 16 2021 at 14:04):While eg the seL4 proofs are closer to "applications"
Paolo Giarrusso (Nov 16 2021 at 14:05):Even if it's true that they could have more clients than a typical application, in principle.
Paolo Giarrusso (Nov 16 2021 at 14:05):Also you're entitled to care more for open-source libraries than proprietary applications!
Karl Palmskog (Nov 16 2021 at 14:06):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
Paolo Giarrusso (Nov 16 2021 at 14:09):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 :-)
Paolo Giarrusso (Nov 16 2021 at 14:09):anyway, sorry for dragging us into such a wild OT!
Karl Palmskog (Nov 16 2021 at 14:10):I broke off the topic a bit to fix that. I guess we can move to Coq users also.
Notification Bot (Nov 16 2021 at 14:11):This topic was moved here from #Coq Platform devs & users > Testing with multiple OCaml versions by Karl Palmskog
Karl Palmskog (Nov 16 2021 at 14:14):@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
Paolo Giarrusso (Nov 16 2021 at 14:16):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”.
Karl Palmskog (Nov 16 2021 at 14:16):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
Paolo Giarrusso (Nov 16 2021 at 14:16):I don’t disagree!
Karl Palmskog (Nov 16 2021 at 14:17):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 native_compute!
Paolo Giarrusso (Nov 16 2021 at 14:17):TCB-wise, all I _can_ say is that our C++ axioms are already public, even if under the license you don’t like
Paolo Giarrusso (Nov 16 2021 at 14:19):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
Karl Palmskog (Nov 16 2021 at 14:19):well, is there a public axiom validation? E.g., empirical evidence this actually capture what C++ compilers are doing, etc.
Karl Palmskog (Nov 16 2021 at 14:21):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
Paolo Giarrusso (Nov 16 2021 at 14:22):I’m pretty confident you would not yet be satisfied
Paolo Giarrusso (Nov 16 2021 at 14:23):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 :-)
Karl Palmskog (Nov 16 2021 at 14:24):OK, sure, I was just asking about "does there exist something like X that is public"
Paolo Giarrusso (Nov 16 2021 at 14:27):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.
Paolo Giarrusso (Nov 16 2021 at 14:27):(we’re currently polishing these docs up)
Karl Palmskog (Nov 16 2021 at 14:29):is the scope of the axioms functional/behavioral only or do you consider non-functional properties (information flow, memory space, ...)?
Paolo Giarrusso (Nov 16 2021 at 14:30):thankfully, our internal setup allows us to progress on verification without a finished C++ semantics…
Paolo Giarrusso (Nov 16 2021 at 14:31):I’d say functional-only
Karl Palmskog (Nov 16 2021 at 14:34):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".
Paolo Giarrusso (Nov 16 2021 at 14:34):anyway, I’m not yet going to argue this semantics is “correct” yet; count this as a “release early, release often” version.
Paolo Giarrusso (Nov 16 2021 at 14:35):“conflict resolution”? conflicts between bits or humans?
Karl Palmskog (Nov 16 2021 at 14:35):conflicts between humans about adopting protocols and the like ("most verified wins")
Karl Palmskog (Nov 16 2021 at 14:36):well, going from a 2000-page(?) language spec in English down to hundreds/thousands of Coq lines seems worthwhile
Karl Palmskog (Nov 16 2021 at 14:37):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)
Ana de Almeida Borges (Nov 16 2021 at 14:42):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...
Paolo Giarrusso (Nov 16 2021 at 18:15):Non-minimal bug reports are IMHO better than nothing, @Ana de Almeida Borges
Last updated: Jan 27 2023 at 02:04 UTC