Whats the advantage of having FLOSS code, proofs (including specifications), and evidence?
Publishing unchangeable implementations (including specifications and code) are much less useful as examples. We want developers, tool-builders, teachers, and even students to build on the examples, and have the examples improve over time. Indeed, we want at least some examples to grow into useful programs where appropriate. Besides, the environment changes over time, new FM techniques are discovered (and must be tried out), and requirements change too. That implies that FLOSS examples will be much more valuable than unchangeable “source available” programs.
