It's important to know that (in the usual setting of analysis) not every function is everywhere (or even anywhere) differentiable, but this is more orthogonal to the author's point than opposed to it. A square wave is piecewise differentiable and you can compute a piecewise derivative. The Weierstrass function is defined by an infinite series, and you can compute its derivative term-by-term by the usual rules and check that the result does not converge; it is indeed straightforward to calculate its nonexistent derivative, and this is what Weierstrass did!
In general, to even ask what it means to compute a derivative we need to specify some input language which describes functions in finite terms; we are necessarily in the world of constructions rather than (say) arbitrary set-theoretical maps between infinite sets. With this in mind, the claim that differentiation is always a straightforward computation is a strong one.
Fwiw, you can use the "Modern English" language setting to banish the long s. Reproducing Byrne's original typography is a stated goal of the author. (You can certainly debate the value of that goal.)
Apple may not design for repairability, but what you are saying is not true. I have personally purchased and installed genuine replacement displays on MacBooks with no involvement from Apple.
Apple publishes repair guides for this (e.g., https://support.apple.com/en-us/120768) as does iFixit. Genuine parts are available for purchase and tools are available to rent by individuals (see https://support.apple.com/self-service-repair, which specifically mentions display replacement). Skill and patience are required; replacement by Apple is not.
The etymology and physical metaphor of "The Singularity" are a bit confused here, and I think it muddles the overall point.
> the singularity is a term borrowed from physics to describe a cataclysmic threshold in a black hole
In his article which popularized the idea of The Singularity, Vinge quotes Ulam paraphrasing von Neumann, and states, "Von Neumann even uses the term singularity". As von Neumann surely knew, "singularity" was a term widely used in mathematics well before the idea of black holes (etymonline dates first use to 1893). Vinge does not say anything about black holes.
> an object is pulled into the center [of] gravity of a black hole [until] it passes a point beyond which nothing about it, including information, can escape. [...] This disruption on the way to infinity is called a singular event – a singularity.
The point at which "nothing" can escape a black hole is the event horizon, not the singularity. What exactly happens to information and what exactly happens when crossing the event horizon are subjects of debate (see "black hole information paradox" and "AMPS/firewall paradox"); however, it's probably fair to say that the most orthodox/consensus views are that information is conserved through black-hole evaporation and that nothing dramatic happens to an observer passing through the event horizon.
> the singularity became a black hole, an impenetrable veil hiding our future from us. Ray Kurzweil, a legendary inventor and computer scientist, seized on this metaphor
While I'm not prepared to go into my personal views in this comment, it's worth noting that the idea that "exponential curves look the same from every point" is not foreign to, e.g., the Kurzweilian view of The Singularity; nevertheless, fitting dramatic, industrial-revolution-sized progress into the fixed scale of a (contemporary) human lifetime would surely be a big deal. This idea, (whether you believe it will happen or not), is obscured by the spurious black hole metaphor.
It's true that in intuitionistic logic "A implies (A or B)"; the usual computational interpretation of that is that "there is a function taking a value of type A and returning a value of type A + B", where + is the tagged union, and, per above, that function is exactly the one which tags its input as belonging to the left disjunct.
I suspect you are still reading "A implies B" as "A is a subtype of B", derived from a set-theoretic interpretation of propositional logic. But the constructive interpretation is that a proof of "A implies B" is a method to take a proof of A and transform it into a proof of B. Computationally, a value of type "A implies B" (typically rewritten "A -> B") is a function that takes values of type A and returns values of type B.
I suppose I erroneously assumed some familiarity with the correspondence between product types (i.e., types of pairs) and the constructive logical interpretation of "and".
Suffice it to say for now: there is an interpretation of logic that gives a tighter correspondence to programming than the set-theoretic one, under the name "Curry-Howard" or "propositions as types, proofs as programs", and which has been known and cherished by logicians, programming language theorists, and also category theorists for a long time. The logic is constructive as it must be: a program of type A tells us how to build a value of type A, a proof of proposition A tells us how to construct evidence for A. From here we get things like "a proof of A and B is a proof of A together with a proof of B" (the "BHK interpretation"), which connects "and" to product types...
I spoke up because I could not leave untouched the idea that "tagged unions are illogical". On the contrary, tagged unions (aka "disjoint unions", "sum types", "coproducts", etc.) arise forthwith from an interpretation of logic that is not the set-theoretical one, but is a more fruitful one from which programming language theory begins. You are not wrong that there is also a correspondence between (untagged) union and intersection types and a set-theoretical interpretation of propositional logic, and that union and intersection types can also be used in programming, but you are missing a much bigger and very beautiful picture (which you will find described in most any introductory course or text on PL theory).
Well, I have outlined the usual story of logic as it corresponds to programming (as has been accepted for at least some five decades now); it strains credulity to claim that logic is illogical.
Now I do see where you are coming from; under a set-theoretic interpretation with "implies" as "subset", "or" as "union", and "and" as "intersection", the fact that "A implies (A or B)" tells us that an element of the set A is also an element of the set "A union B".
However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.)
So "implies" should not be read programmatically as a subtyping relation; instead, "A implies B" tells us that there is a function taking a value of type A to a value of type B. In the case of "A implies (A or B)", that function takes its input and tags it as belonging to the left disjunct!
Another perspective I must mention: given a proof of "A or B" and another of "(A or B) implies C", how can we combine these into a simpler proof of just "C"? A proof of "(A or B) implies C" must contain both a proof a "A implies C" and a proof of "B implies C", and we could insert into one those proofs a proof of A or a proof of B. But we have to know which one we have! (This is a very short gloss of a much deeper story, where, under Curry-Howard, proof simplification corresponds to computation, and this is another way of describing a function call that does a case-analysis of a tagged union (or "sum type").)
Now "union and intersection" types with the set-theoretic properties you are hinting at have indeed been studied (see, for example, Section 15.7 of Pierce's "Types and Programming Languages"). But they do not replace the much more familiar "sum and product types", and do not play the central role of "or" and "and" in the correspondence of programming to logic.
While others have addressed the programming case for tagged unions, I want to add that, to a logician, tagged unions are the natural construct corresponding to "logical or".
In intuitionistic logic (which is the most basic kind from which to view the Curry-Howard or "propositions-as-types" correspondence), a proof of "A or B" is exactly a choice of "left" or "right" disjunct together with a corresponding proof of either A or B. The "choice tag" is part of the "constructive data" telling us how to build our proof of "A or B". Translated back into the language of code, the type "A | B" would be exactly a tagged union.
In general, to even ask what it means to compute a derivative we need to specify some input language which describes functions in finite terms; we are necessarily in the world of constructions rather than (say) arbitrary set-theoretical maps between infinite sets. With this in mind, the claim that differentiation is always a straightforward computation is a strong one.