It looks like you're making a good argument for a different conversation or tangent to this one. The comment you replied to was aimed at Guido van Rossum's clai

It looks like you're making a good argument for a different conversation or tangent to this one. The comment you replied to was aimed at Guido van Rossum's claim up-thread that formal verification was useless and couldn't help his OS. I countered that claim. You're now saying techniques in published papers aren't beneficial without source. I'll address that since you took time to write it. Actually, let's look at not publishing CompCert's source as an example. Under your theory, I can't learn anything at all from just the paper or binary. Here's what I think I can learn from it: 1. They claim they verified most of C language in a compiler down to the assembly in Coq. John Regehr's testing confirms it has the correctness in terms of defects detected that one would expect in a verified compiler. So, now I know (a) they did do a verified compiler for C, (b) the methods they describe might help other formal developers in their verifying compiler work (give ideas at minimum), (c) a successful verification of a C compiler clears the way for more projects/funding on C or other compilers, and (d) anyone needing a verified C compiler has a supplier, AbsInt, whose work was rigorously evaluated. 2. Building on former, the fact that the compiler will produce correct output more than most compilers means it can be used to check correctness of highly-optimizing compilers. Automated testing can be directed at an optimizing compiler and CompCert where the output of programs run through each is checked for equivalence. If not equal, probably a bug in the unverified one but maybe CompCert itself. Likewise, I considered re-running a pile of test cases for a C program that were showing bugs through CompCert version of that same program. Any bugs disappearing might mean those were compiler bugs. Help narrow things down. 3. A key method for both CompCert and CakeML was using a series of intermediate languages working from highest to lowest level w/ equivalence checks on each pass. People doing formal or informal methods for developing compilers can then apply that technique, maybe even those DSL's, to see if it improves their own work. They might start creating their own DSL's. If Racket and Red are any hint, just giving the ability to do DSL's with worked examples can lead to productivity or correctness improvements in many types of software. Let's look at another example from high-assurance security. One of the demonstrators was closed-source GEMSOS. Its design and assurance methods are described here: http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf I used such papers to develop solutions that were highly resistant to penetration because the techniques supporting them naturally lead to that. Especially little code in TCB, using FSM's to brute-force the analysis, input validation, avoiding pointers much as possible, safer language, and so on. Difference between popular/mainstream INFOSEC and what I learned from INFOSEC's founders in high-assurance was mind-blowing. Common example is covert-channel analaysis of OS's is almost non-existent but Kemmerer's paper tells you how (Shared Resource Matrix). Likewise, highly-secure repo's are uncommon but Wheeler's survey (SCM Security) tells you how to fix it. Heck, I even learned to make sure my stuff could be formally verified later by just reading what was easy, moderately difficult, or hard in formal methods papers. I called Design for Verification which I later found was similar to how hardware engineers do things (i.e. DFT, DFM). I learned that from reading on Cleanroom methodology where they verified simplified code in box structures by eye before building for test runs. So, I reject based on worked examples the claim that it's "not helpful" to have papers w/out source code that describe worked examples in enough detail to replicate for critical review or use for new project. It's been very helpful to all kinds of people. I also agree with you that there's many reasons to prefer source and/or data used in research over black boxes. It's good they published the source of CompCert. Even better that CakeML is fully open versus CompCert's restrictions. As I hinted at in 1, other teams started using CompCert and CakeML as backend infrastructure for their own work on other languages. Them being commercial w/ free use for researchers would probably have reduced adoption but I bet there still would be some if their DSL's were published. People could still do useful things, push state-of-the-art, and publish the work with much fan fare. So, still benefit even if not maximal benefit to have detailed papers with no source.