Rob, the problem I have with things like "type theory" and "category theory" is that they almost always elide their foundation in HOL (high order logic) which means they don't *really* admit that they are syntactic sugars for second-order predicate calculus. The reason I describe this as "risible" is the same reason I rather insist on the Algorithmic Information Criterion for model selection in the natural sciences:
Reduce the argument surface that has us all going into hysterics over "truth" aka "the science" aka what IS the case as opposed to what OUGHT to be the case. Note I said "reduce" rather than "eliminate" the argument surface. All I'm trying to do is get people to recognize that *relative to a given set of observations* the Algorithmic Information Criterion is the best operational definition of the truth. It's really hard for people to take even this *baby* step toward standing down from killing each other in a rhyme with The Thirty Years War, given that social policy is so centralized that everyone must become a de facto theocratic supremacist as a matter of self defence. It's really obvious that the trend is toward capturing us in a control system, e.g. a Valley-Girl flirtation friendly interface to Silicon Chutulu that can only be fought at the physical level such as sniper bullets through the cooling systems of data centers. This would probably take down civilization itself given the over-emphasis on efficiency vs resilience in civilization's dependence on information systems infrastructure. On Thu, May 16, 2024 at 10:36 PM Rob Freeman <chaotic.langu...@gmail.com> wrote: > James, > > For relevance to type theories in programming I like Bartosz > Milewski's take on it here. An entire lecture series, but the part > that resonates with me is in the introductory lecture: > > "maybe composability is not a property of nature" > > Cued up here: > > Category Theory 1.1: Motivation and Philosophy > Bartosz Milewski > https://youtu.be/I8LbkfSSR58?si=nAPc1f0unpj8i2JT&t=2734 > > Also Rich Hickey, the creator of Clojure language, had some nice > interpretations in some of his lectures, where he argued for the > advantages of functional languages over object oriented languages. > Basically because, in my interpretation, the "objects" can only ever > be partially "true". > > Maybe summarized well here: > > https://twobithistory.org/2019/01/31/simula.html > > Or here: > > > https://www.flyingmachinestudios.com/programming/the-unofficial-guide-to-rich-hickeys-brain/ > > Anyway, the code guys are starting to notice it too. > > -Rob > > On Fri, May 17, 2024 at 7:25 AM James Bowery <jabow...@gmail.com> wrote: > > > > First, fix quantum logic: > > > > > https://web.archive.org/web/20061030044246/http://www.boundaryinstitute.org/articles/Dynamical_Markov.pdf > > > > Then realize that empirically true cases can occur not only in > multiplicity (OR), but with structure that includes the simultaneous (AND) > measurement dimensions of those cases. > > > > But don't tell anyone because it might obviate the risible tradition of > so-called "type theories" in both mathematics and programming languages > (including SQL and all those "fuzzy logic" kludges) and people would get > really pissy at you. ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/T682a307a763c1ced-M2f546f083c9091e4e39fabc8 Delivery options: https://agi.topicbox.com/groups/agi/subscription
