> Also, this pinged a few neurons deep in my memory, so I found what it made me remember. Back in 2004, some random named Jeff V. Merkey tried to buy a special license to the then-current kernel for $50,000.00:
> In response, Molnar did some quick sloccount math and estimated the kernel as being worth $175,974,824 at that time.
Absolutely.
Just to clarify: Molnar first did the quick sloccount math and estimated $176 million USD. However, Molnar used the estimation values appropriate for an application.
But in fact, operating systems kernels are known to be more difficult to develop than typical applications. So I used the same approach but refined it to use parameters appropriate for a kernel. The article https://dwheeler.com/essays/linux-kernel-cost.html is really a response to Molnar's work; he did a rough estimate, I did a slightly-more-refined estimate. Those additional tweaks resulted in a higher redevelopment cost of $612 million (USD). Which gave the $50,000 offer an even bigger contrast.
The real point was that, even if it would have been possible accept $50K, it was absurdly low. You could argue about the estimate for a factor of 2, or 10, or even 100, and it still wouldn't change anything. Merkey was free to lowball a proposal, but that doesn't mean it should be accepted :-).
There was a 2004 article about this in LWN.net. LWN.net, and many others, don't see how such an offer could have been legally enforcible anyway, since you'd have to get the agreement of all the kernel contributors: https://lwn.net/Articles/106353/
To me, the kernel offer was more of an opportunity to find a way to measure the size of a kernel in a way that matters to people. Lines of code, or bytes on disk, don't really mean much to most people. Money... does :-).
in fact, operating systems kernels are known to be more difficult to develop than typical applications.
I'm not convinced. The core OS kernel code, sure; but more than half of the Linux kernel is drivers, and those are not just applications but separate applications; a change in an Intel wifi driver is unlikely to interact in any way with the nvme driver.
> I'm not convinced. The core OS kernel code, sure; but more than half of the Linux kernel is drivers ...
I agree that more than half of the Linux kernel is drivers. In fact, in my analysis of Red Hat 7.1 at https://dwheeler.com/sloc/redhat71-v1/redhat71sloc.html I found that 57% of the Linux kernel was in the drivers subdirectory. Obviously that varies over time. So I completely agree with that part!
> and those are not just applications but separate applications; a change in an Intel wifi driver is unlikely to interact in any way with the nvme driver.
They aren't really separate applications, though. More importantly, that's not the primary effort (and cost) driver for this effort estimation model. I used the COCOMO model, an effort estimation model that was publicly available and widely used at the time. I then applied its rules to the Linux kernel of that time, as best I could. I discussed every parameter I set, and why, here: https://dwheeler.com/essays/linux-kernel-cost.html
Here are some of the reasons why kernel code takes more effort, per the model:
* It inherits some of the general challenges of writing embedded software. There's very little in the way of a safety net (this is the safety net), and it's closer to the bare metal. You're writing in C (or later in Rust), not a language that shields you from many challenges. In COCOMO parlence this code is "semidetached".
* RELY: Required software reliability: High (1.15). The Linux kernel developers care a lot about reliability, which takes longer.
* CPLX: Product complexity: Extra high (1.65). "The kernel must perform multiple resource handling with dynamically changing priorities: multiple processes/tasks running on potentially multiple processors, with multiple kinds of memory, accessing peripherals which also have various dynamic priorities. The kernel must deal with device timing-dependent coding, and with highly coupled dynamic data structures (some of whose structure is imposed by hardware). In addition, it implements routines for interrupt servicing and masking, as well as multi-processor threading and load balancing. And yes, that includes drivers; drivers must handle threading and other challenges that "normal" code doesn't, because the driver code is where those complexities are handled."
* TIME: Execution time constraint: High (1.11). "Although it doesn’t need to stay at less than 70% resource use, performance is an important design criteria, and much effort has been spent on measuring and improving performance."
* VIRT: Virtual machine volatility: High (1.15). "The most common processor (x86) doesn’t change that quickly, though new releases by Intel and AMD do need to be taken into account [but] the other components of underlying machines (such as motherboards, peripheral and bus interfaces, etc.) change on a weekly basis. Often the documentation is unavailable, and when available, it’s sometimes wrong (which from a developer’s point of view looks like a volatile interface, since it keeps changing). The Linux kernel developers spend a vast amount of time identifying hardware limitations/problems and working around them. What’s worse, there’s a variety of different hardware, and new ones keep arriving... the interface of the underlying machine is actually quite volatile."
Not every factor makes things worse. The people analyzing it (ACAP) and developing the code (PCAP) are unusually capable, with high experience in the programming language (LEXP) and modern development practices (MODP). But these only partly compensate for the fundamental challenge of writing highly performant kernel code.
Anyway, that's my rationale. I did this back in 2004, so I was necessarily using data and models available at the time. Most importantly, I think its key point was absolutely correct: it would have cost far more than $50,000 USD to re-develop the Linux kernel of that time.
They aren't really separate applications, though. More importantly, that's not the primary effort (and cost) driver for this effort estimation model. I used the COCOMO model, an effort estimation model that was publicly available and widely used at the time. I then applied its rules to the Linux kernel of that time, as best I could.
COCOMO says that the cost scales superlinearly with the number of SLoC; my point is that drivers scale linearly because they're effectively separate projects. (In fact, to the extent that they're not separate projects, the cost in fact scales sublinearly since there's a bunch of code being copied and pasted when new drivers are written.) Your tool has this "--multiproject" concept; a better estimate would have identified which parts of the tree (primarily drivers) were functionally separate from the rest of the kernel.
I think its key point was absolutely correct: it would have cost far more than $50,000 USD to re-develop the Linux kernel of that time.
Oh, absolutely. I'm not disputing the conclusion; just the claim that an OS kernel is inherently more complex than another application of the same size.
> COCOMO says that the cost scales superlinearly with the number of SLoC; my point is that drivers scale linearly because they're effectively separate projects. (In fact, to the extent that they're not separate projects, the cost in fact scales sublinearly since there's a bunch of code being copied and pasted when new drivers are written.) Your tool has this "--multiproject" concept; a better estimate would have identified which parts of the tree (primarily drivers) were functionally separate from the rest of the kernel.
If all drivers were essentially completely independent projects that never interacted with each others, then yes, I'd agree that multiproject would be a better model. And if each was mainly a copy-and-paste of another, then it'd definitely be sublinear.
However, I have a very different expectation. In the Linux kernel, there's a strong pressure to try to create common interfaces that different drivers support. There's also pressure to create common lower-level functions that everyone can call. This reduces total code and reduces long-term maintenance, but ends up creating more interlinkages because the drivers are NOT really isolated separate projects at all. Maybe the drivers start somewhat independent, though I'm skeptical of even that, but I think that's not at all where they stay.
Let's get specific. The Linux kernel groups similar hardware into distinct subsystems. This includes networking, input subsystem (keyboards/mice/etc.), ALSA (sound), V4L2 (webcams/video capture cards), and GPIO.
Each subsystem defines a unified programming interface using standard data structures and callback functions. Drivers are typically split into a core framework that handles general logic and low-level portions. Driver developers plug into the existing framework for common features like power management and buffering. These interfaces often change as new drivers are created that require changes to the interface.
Because in practice there's a lot of interaction among drivers, I would not expect that, after years of driver development, the different drivers would really be independent. Indeed, many have asked the Linux kernel developers to make it easy to have completely separate and isolated drivers, but the developers have resisted because they believe it's important to have the drivers integrated into the kernel to support that kind of constant collaboration between drivers.
It'd be cool to see an analysis to settle the question. Future research for someone else I suppose :-).
> I consider this a simplistic analysis, because a closed-source Linux with a straightforward monetary pricetag would be worth a lot less in practice, since it would cease to be the de-facto OS for pretty much all new hardware products.
It's necessarily an estimate, of course. The best way to get effort figures would be to record every minute used for development, and the best way to get cost figures would be to re-develop from scratch. That wasn't practical, so using a widely-accepted estimation system seemed like a reasonable approach.
It's true that this analysis doesn't tell you the purchase price. However, I wasn't trying to estimate the purchase price. I was trying to estimate the cost to develop the software, if it had been developed using traditional closed source practices. If Linux had been developed by a for-profit organization to make a profit, the organization would have planned on charging more that that (in aggregate among all its users), since otherwise they'd be knowingly developing the software at a loss. That doesn't mean that the company actually could have charged this, as it often happens that products don't make a profit, but that's different from intent. And this is all different from value. If a product has value to you that's more than it costs to get, then economically you should consider getting it.
No matter what, these time and money figures can only be rough estimates. However, I think they were useful, because they destroyed a false assumption many had at the time.
In the 1980s and 1990s many people presumed that large-scale systems could NOT be developed as open source software. People did sometimes share software, but it was widely assumed that this could only be successful for small programs. The term "open source software" didn't even exist until 1998. The term "free software" was coined in the early 1980s, so that definitely was a discussion point. However, many people didn't think you could build larger systems with software licensed that way.
Bill Gates published in 1976 his "Open Letter to Hobbyists" that crystallized this argument. He claimed that if software was freely shared it would prevent the writing of good software. He basically argued that closed source software development (not a term of the time) was necessary.
The point of my paper was to show that it was possible to build larger software systems without being closed source software. Even at the time, people were being paid to develop some of that software, but the point was that sharing of software under a generous license did not end software development at all. I think my paper did the job. You can argue many things, but no one argues that open source software cannot be used to build big systems. We have existing systems, measureably large, that refute the claim.
Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
The cables are supposed to be labelled with their maximum speed (5, 10, 20, 40, or 80 Gbps or nothing if no data) and maximum wattage (60W or 240W).
HOWEVER, I don't remember ever seeing a cable with such a label. I'm sure they exist, but I don't see them. Requiring products to be labelled, and treating mislabelling as fraud, could mostly solve this. It's definitely a real problem.
> Requiring products to be labelled, and treating mislabelling as fraud, could mostly solve this.
There are too many manufacturers to hunt. Basically USB-IF needs to stop almost all shipments in the world. That's not going to happen.
USB spec is completely open and free to obtain. While it allows people to develop and DIY many things, it also attracts bad manufacturers like flies.
Good certified cables with correct markings exist. There are companies like Cable Matters or Startech who bother to actually certify their cables and get USB-IF TIDs. They do cost you quite a bit money though. Here are some:
In Metamath the proofs hide absolutely nothing. There's no hand-waving "it's obvious that". Every step in a proof must be rigorously and directly proven by some axiom or a previously-proven theorem with absolutely no exceptions. This also means that while finding proofs can be hard, verifying proofs is fast. I just ran a proof verification run of over 47,000 theorems in 6.35 seconds. In the Metamath Proof Explorer / set.mm database (the one with classical logic and ZFC), we routinely run multiple provers by different people on every proposed change. So not only is the kernel small, it's implemented by multiple different programs, making it extremely unlikely we'll accept an invalid proof.
Metamath is interesting for education in the principles of formal proofs, because:
1. The Metamath Book is self-contained well written, simple introduction.
2. Everything is explicit, nothing is hidden.
3. Because of extremely simple syntax and semantics it's easy write own proof verifier.
The drawbacks are:
1. Non-standard approach to free and bound variables.
2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.
3. Almost no proof automation. No tactics. Long, hard to read proofs.
I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.
What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL
Reading `hol.mm` made me grateful for Lean 4's general purpose programming.
I get the string substitution focus, and respect what metamath has achieved, but the bridge Lean 4 makes wrt systems programming has left quite an impression.
I wonder how many people mostly see mathlib4 & think that's the one prescribed route (ala Rust) when one of Lean 4's under-documented super powers is the ease with which you can roll your own light-weight low to zero overhead domain-specialized constructs that are also trivial to prove because of the dependent type system.
(Perhaps more for verified functional systems than deep math.)
There are other forms of logic? is intuitionistic logic as rigorous? fascinating
edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!
> if it is weakened, how can you prove the same stuff?
Sometimes, you can't. In particular, so-called "non-constructive" proofs don't work in intuitionistic logic. Some mathematicians like to work in intuitionistic logic: for philosophical reasons, pragmatic technical considerations, or just because they think it's interesting.
This is not entirely true: non-constructive proofs can be fully understood within intuitionistic logic as proofs of negative statements, viz. statements about what isn't constructively true or doesn't constructively exist. From this point of view, intuitionistic logic can be seen as stronger and more powerful than classical logic, because it can endow positive statements (particularly statements about logical disjunctions or existentials) with computational content whenever they have a direct proof.
Classical logic doesn't bother with this; positive and negative statements are completely dual to one another, and this duality is elegant in its own way (as people who are committed to classical logic will readily point out), but one needs linear logic in order to combine it with an awareness of constructive statements.
Intuitionistic logic can prove less than classical logic, but what you gain is that proofs are constructive. Also you can use it to reason about things for which law of excluded middle doesn't hold (typically types).
I love this, and more generally the Triptych Project. We shouldn't need to use JavaScript to work around important limitations in HTML that are widely needed.
> https://dwheeler.com/essays/linux-kernel-cost.html
> In response, Molnar did some quick sloccount math and estimated the kernel as being worth $175,974,824 at that time.
Absolutely.
Just to clarify: Molnar first did the quick sloccount math and estimated $176 million USD. However, Molnar used the estimation values appropriate for an application.
But in fact, operating systems kernels are known to be more difficult to develop than typical applications. So I used the same approach but refined it to use parameters appropriate for a kernel. The article https://dwheeler.com/essays/linux-kernel-cost.html is really a response to Molnar's work; he did a rough estimate, I did a slightly-more-refined estimate. Those additional tweaks resulted in a higher redevelopment cost of $612 million (USD). Which gave the $50,000 offer an even bigger contrast.
The real point was that, even if it would have been possible accept $50K, it was absurdly low. You could argue about the estimate for a factor of 2, or 10, or even 100, and it still wouldn't change anything. Merkey was free to lowball a proposal, but that doesn't mean it should be accepted :-).
There was a 2004 article about this in LWN.net. LWN.net, and many others, don't see how such an offer could have been legally enforcible anyway, since you'd have to get the agreement of all the kernel contributors: https://lwn.net/Articles/106353/
To me, the kernel offer was more of an opportunity to find a way to measure the size of a kernel in a way that matters to people. Lines of code, or bytes on disk, don't really mean much to most people. Money... does :-).
reply