The Eternal Doorman

This idea about elaborating relations under constraints is really interesting. See  Thorsten Altenkirch on NaÏve Type Theory and An Interesting and Useful Duality  and  Condensing Programs .    See miniKanren, live and untagged: quine generation via relational interpreters (programming pearl) by William E. Byrd, Eric Holk and Daniel P. Friedman and  https://minikanren.org/  for more on Micro Kanren ( 21:00 ). See also  What is Formal Logic?  and  Nada Amin - Metacircular Interpretation ad infinitum . Subscribe to Strange Loop . Subscribe to  RIO HOLIC .

Subscribe to Sakara .

See An extreme North Atlantic Oscillation event drove the pelagic Sargassum tipping point by Julien Jouanno, Sarah Berthet, Frank Muller-Karger, Olivier Aumont and Julio Sheinbaum and also Productivity, growth, and biogeochemistry of pelagic Sargassum in a changing world by Brian E. Lapointe, Deanna F. Webber and Rachel A. Brewton. Subscribe to Anton Petrov . It must have been bacteria and algae like this that created the atmosphere we have today. There is a 1.5 billion year gap between the Great Oxidation Event and the appearance of the first photo-synthesizing plants. My comment : Wow, I had no idea how grateful I should be that I don't live in a regime of mass-independent isotope fractionation!!! I would like to hear something about the dynamics of the system that came out of that event. It seems like some sort of homeostasis was reached. Subscribe to GEO GIRL .

  He did a nice one about Langton's Ant too: He has written a 25 page paper on his path theorem: Finite-Support Periodic Highways of Langton's Ant . Subscribe to rand.nerdAJ .

Subscribe to Miranda Lambert .  Subscribe to Daniela Spalla . Subscribe to Pomme .

Two talks given in 2014 at Indiana University. I've never heard him talk directly about computation and software before ( 12:59 ). It's really interesting. I hope Douglas Hofstadter was in the audience. See  What is Formal Logic?  I wish George Ellis had heard it too. See Why is Physics So Difficult? 23:06 He points out that syntactic structure is observer-relative: it requires someone to interpret the machine state as representing some formal structure in a certain context, and this context is almost always ignored. My comment :  54:05 It's interesting that he returns to molecules and their observer-independent reality to explain by analogy his position on consciousness as a physical effect. The thing is that most of the particular properties of water are not reducible to properties of the molecules alone, but only in terms some of higher-level organisation. I think the observer-independent existence of molecules is not that far from the idea of an observer-independent...

This is an idea about a different way to think about programming computers. It's really hard getting the individual bits of a program right so that behaves correctly as a whole. It's not unlike the problem of designing molecules to effect certain metabolic changes in a whole organism. It is much easier to do it the way life works: whole ecosystems adapt to the metabolic regimes induced in the individuals by the conditions in which they live. Adaptation can then be a kind of phase change in the whole system. Phase change is a global condition whereas the metabolic effects of a certain drug are local conditions, depending upon the organisms which ingest it. One of the reasons that modern software systems are so insecure is that they contain enormous amounts of superfluous functionality which can easily be co-opted to other ends. The trick with programming a computer is not just to get it to do some particular thing, it is to get it to do  only  that particular thing, and nothing...

I wrote the blog post yesterday, before I saw this. See Thorsten Altenkirch on NaÏve Type Theory and An Interesting and Useful Duality . 19:09 He mentioned Conor McBride talking about dependent type theory as a revolution. I found this series of 8 talks he did at Cambridge in 2013: Dependently Typed Metaprogramming . The course notes are available here : If you have never met a metaprogram in a dependently typed programming language like Agda [Norell, 2008], then prepare to be underwhelmed. Once we have types which can depend computationally upon first class values, metaprograms just become ordinary programs manipulating and interpreting data which happen to stand for types and operations.   See also  Jesper Cockx - Elaborating Dependent (Co)pattern Matching . Subscribe to About Logic .

See the paper by Jesper Cockx and Andreas Abel:  Elaborating Dependent (Co)pattern Matching . For anyone that wants to understand what Agda is really doing: Subscribe to ICFP Video .