#+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.