Patterson BTFO post

1 files changed, 30 insertions, 0 deletions

diff --git a/staging/modularity/modularity.org b/staging/modularity/modularity.org
new file mode 100644
index 0000000..1648260
--- /dev/null
+++ b/staging/modularity/modularity.org
@@ -0,0 +1,30 @@
+#+TITLE: Modularity is Sheafy
+#+DATE: <2023-11-22 Wed 11:39>
+#+TAGS: Software, Philosophy, Engineering
+
+In my article Software Equals Hardware, I argue that electrical engineers and computer architects have solved the problem of modularity/code-at-scale. However, the discussion of precisely what "modular" means there was, as usual, underspecified to point of error.
+
+On reflection, I feel like a system is modular if it promotes, enhances, or forces things such that some "local" (or small-scale) properties are sufficient to ensure some "global" (or large-scale properties). For example, writing code in a conventional module system carries a set of local restrictions (all code is declared in a module, public functionality in a module needs to be exported, library code needs to be imported, etc.) that together promote a desirable property of the whole codebase (eliminated or much decreased risk of unintentional name collisions). So also for avoiding mutable global state (can't write or alter global variables, but now you can make assumptions about linking), for lexical scope (TODO), and so on. As this looks awful similar to certain structural patterns in mathematics, it led to the formalization:
+
+Modular systems are sheafified.
+
+* The Abstract Nonsense
+
+Of course, unless you're an algebraic geometer, algebraic topologist, or category theorist, this formalization isn't terribly intuitive (and if you are, it isn't terribly formal).
+
+To those schools of wizards is known the concept of a "presheaf:" intuitively, a structure that has some notion of "local" and "global." Obviously, our programs have such a notion; computer scientists tend to call it "scope." By linguistic inference, these wizards also talk about "sheaf;" this means a presheaf that has some way to coherently glue together local structure into global structure. In computer science, we can identify this with composition (which is universally recognized as desirable, even essential to modularity). However, for a given presheaf, there are generally many different sheaves over it (many different ways to compose programs that agree with a given notion of scope).
+
+The wizards save us with a delightfully-named ritual: /sheafification/. There is a way to, for every presheaf on a suitable structure (called a "site"), produce the corresponding sheaf that is, in some sense, the most general (is "left-adjoint to the inclusion functor of sheaves into presheaves," whatever that means). Therefore, if we design programs such that our composition agrees with the most general composition our notion of scope induces, we can expect to get the most general programs.
+
+Note: the sheafification still allows for freedom in two dimensions: the choice of what the underlying structure is, and the choice of what locality means. We must appeal to additional philosophical and practical concerns to get a unique definition of "modular," but it cannot be overstated how valuable the restriction of the debate to those two choices is.
+
+* Its Application
+
+It would be really nice if we could use this definition to actually /discover/ modular abstractions, or to /prove/ that a given abstraction is maximally modular. The former I'll leave to the reader; to bolster this definition, here are several cases in which the received wisdom on modular design aligns with its predictions.
+
+** Module Systems
+
+The problem here is: we've written a bunch of code libraries, and we want to have a way to call functions from the libraries
+
+** Scoping Rules
+**