Laurie Wired on Richard Gabriel's 35-year-old essay "Worse Is Better"

It sounds like Richard Gabriel is the inventor of the term Software Architecture. See his 1996 book Patterns of Software. See https://dreamsongs.com/.

In answer to her question at the end: I think the best thing is to make stuff better and better. So for example, I think it would be nice if Lean's Mathlib one day proved the Generalised Stokes Theorem on differential manifolds and derived the proofs of the Fundamental Theorem of Calculus from that. At the same time, it would be nice if people could work on teaching the basic ideas of simplicial forms and cohomology to high school students so they could understand the Generalised Stokes Theorem in simplicial complexes before they were taught how to do epsilon-delta proofs of calculus on the real line. In computer science, the equivalent process is one where, instead of designing new languages like C++ and Lean and producing a never-ending stream of concrete implementations that are all different, people specified the languages in a formal structure which lifts the work to the highest level of abstraction where it it is meaningful. Then the result would be, I imagine, one single finitely presented algebraic structure that captures all of the state of knowledge. See 3:43 in the following talk by William Lawvere.

Subscribe to Laurie Wired.

 

See Vladimir Voevodsky - What if Current Foundations of Mathematics are Inconsistent. 

Subscribe to Matt Earnshaw.

I just noticed I forgot to put the question mark at the end of that title of Voevodsky's, then I thought, why not leave it out? It's a curious fact that intuitionistic logic, because it is more conservative about what it proves, is more extensible than classical logic. For example, because Heyting Arithmetic (HA) is intuitionistic and does not admit the law of the excluded middle, you can consistently extend HA with the axiom ¬consistent(HA) then the resulting theory HA + ¬consistent(HA) is inconsistent, but it cannot prove that fact, nor can it derive anything that ordinary Heyting Arithmetic could not derive, apart from trivial conjunctions of the extra axiom with other statements provable in HA. Classical logic on the other hand can not be consistently extended to the same extent, because it can prove more theorems using the Law of the Excluded Middle. It follows from this that a framework for the study of Intuitionistic logic can also be used for the study of Classical logic, because the Classical logic is a strictly smaller theory than Intuitionistic logic.