blob: 10c07f969ac2b002ec091bd38ee08cd2b4070a5f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
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.
|
