From d4ed7d7df524e397fbcdae5e25e1e13b4f10b4a3 Mon Sep 17 00:00:00 2001 From: Yuchen Pei Date: Thu, 17 Feb 2022 19:40:10 +1100 Subject: added some microposts --- microposts/big-nonfree-gotcha.org | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 microposts/big-nonfree-gotcha.org (limited to 'microposts/big-nonfree-gotcha.org') 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. -- cgit v1.2.3