diff options
Diffstat (limited to 'microposts/big-nonfree-gotcha.org')
| -rw-r--r-- | microposts/big-nonfree-gotcha.org | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/microposts/big-nonfree-gotcha.org b/microposts/big-nonfree-gotcha.org new file mode 100644 index 0000000..10c07f9 --- /dev/null +++ b/microposts/big-nonfree-gotcha.org @@ -0,0 +1,26 @@ +#+title: Big nonfree gotcha +#+date: <2022-02-10> + +I just came across my first big nonfree gotcha in formal verification. + +[[https://compcert.org/][CompCert]], the verified C compiler, is nonfree. + +And I learned there are no free alternatives. + +And opam (the ocaml package manager) installed it without any warning, +possibly as a dep of VST, used in [[https://softwarefoundations.cis.upenn.edu/vc-current/index.html][Vol 5 of Software Foundations, +Verifiable C]]. + +But I also learned that the part of CompCert required for the study of +Verifiable C is free. Someone should definitely extract out the free +part which I hope can be distributed on opam as say "compcert-free". + +On a side note, I feel the GNU Project is missing some essential +functional packages, which could result in the proglang / formal +verification community having less aspirations for free software. I +am not faulting the GNU Project for this, of course. But by contrast, +all Emacs packages, be it independent or part of the GNU ELPA, are by +default licensed under GPLv3+, which could be caused by the GNU +Project having a strong foothold in Emacs. + +H/t Kiran G and pgiarrusso. |