The logical deductions in the opening section are solid, but consider a Bayesian perspective. Given two extensionally equivalent programs which implement the same algorithm, with the only difference being that one has source available and one does not, the source-available program is likelier to receive bug fixes. This is an instance of Linus’ law. Note a corollary: programs written directly in low-level machine code are effectively programs without high-level source code, so programs written in higher-level languages are also likelier to receive bug fixes.
The only way to know what a program does when you run it is to…run it.
I like this blunt phrasing of Rice’s theorem. There is a footnote about dependently-typed languages and formal methods which I feel is a misleading hedge; Rice’s theorem does not have exceptions. When a Turing-complete language’s programs are “provably correct at the source level”, this is only because the prover can run a program during compilation, and the proof’s correctness corresponds to the case where the prover halts. Or, more practically, the language under study is split into partial and total regimes, and only the total regime is formally verified; Idris is an example language.
It’s hard to figure out which syscalls and files a large program needs by reading its source…
Note that this complaint is language-specific, unlike most of the article’s context. Languages could be designed which require users to syntactically declare every required syscall in a single central location.
Given two extensionally equivalent programs which implement the same algorithm, with the only difference being that one has source available and one does not, the source-available program is likelier to receive bug fixes. This is an instance of Linus’ law.
Oh absolutely. All other things being equal, having source code is a huge benefit. But other factors are in play. For instance, I’d consider the proprietary Google Chrome or Microsoft Edge more secure than Pale Moon or most webkit2gtk-based browsers.
Note a corollary: programs written directly in low-level machine code are effectively programs without high-level source code, so programs written in higher-level languages are also likelier to receive bug fixes.
This is an interesting perspective that I hadn’t thought of much. I’m reminded of LuaJIT’s maintainability issues: Mike Pell is a brilliant assembly programmer whose LuaJIT optimizations run circles around what GCC/Clang are capable of, but LuaJIT’s future without him is uncertain given a lack of interested devs with the necessary expertise.
Feedback/corrections/dissent more than welcome, esp. from anyone with a reverse-engineering or black-box testing background. I’m happy to edit any errors.
The logical deductions in the opening section are solid, but consider a Bayesian perspective. Given two extensionally equivalent programs which implement the same algorithm, with the only difference being that one has source available and one does not, the source-available program is likelier to receive bug fixes. This is an instance of Linus’ law. Note a corollary: programs written directly in low-level machine code are effectively programs without high-level source code, so programs written in higher-level languages are also likelier to receive bug fixes.
I like this blunt phrasing of Rice’s theorem. There is a footnote about dependently-typed languages and formal methods which I feel is a misleading hedge; Rice’s theorem does not have exceptions. When a Turing-complete language’s programs are “provably correct at the source level”, this is only because the prover can run a program during compilation, and the proof’s correctness corresponds to the case where the prover halts. Or, more practically, the language under study is split into partial and total regimes, and only the total regime is formally verified; Idris is an example language.
Note that this complaint is language-specific, unlike most of the article’s context. Languages could be designed which require users to syntactically declare every required syscall in a single central location.
Oh absolutely. All other things being equal, having source code is a huge benefit. But other factors are in play. For instance, I’d consider the proprietary Google Chrome or Microsoft Edge more secure than Pale Moon or most webkit2gtk-based browsers.
This is an interesting perspective that I hadn’t thought of much. I’m reminded of LuaJIT’s maintainability issues: Mike Pell is a brilliant assembly programmer whose LuaJIT optimizations run circles around what GCC/Clang are capable of, but LuaJIT’s future without him is uncertain given a lack of interested devs with the necessary expertise.
Feedback/corrections/dissent more than welcome, esp. from anyone with a reverse-engineering or black-box testing background. I’m happy to edit any errors.