The Eternal Doorman

From ICFP 2015. See the paper Automatic refunctionalization to a language with copattern matching: with applications to the expression problem by Tillmann Rendel, Julia Trieflinger and Klaus Ostermann and John Reynolds' Definitional Interpreters for Higher-Order Programming Languages .  17:02 Person asking about how you represent infinite streams with finite data. I think the answer is that you use a cyclic data structure. That is the clever trick in Reynolds' defunctionalization transform. See  David MacQueen on his Ideas for Successor ML  and  Open, extensible object models (2006) by Ian Piumarta and Alessandro Warth.  Subscribe to ICFP Video . 

See Petrification in Contemporary Set Theory: The Multiverse and the Later Wittgenstein by José Antonio Pérez-Escobar, Colin Jakob Rittberg and Deniz Sarikaya and Philosophical Investigations into AI Alignment: A Wittgensteinian Framework by José Antonio Pérez-Escobar and Deniz Sarikaya. My comment : 39:54 Our intuition may be more closely tied to language than it seems. There is evidence from linguistics that the kinds of intuition we have about time and space have an intimate connection with the language we speak and even how we write. Lera Boroditsky has done lots of talks about this. The coherence of the foundation, whatever that "actually" is, must ultimately be in our ability as human beings to understand each other's descriptions of their personal direct experience, so in this process of establishing symbols and meanings we will produce various systems, some of which will have more or less rigour than others, depending upon the culture. With...

If you want to emulate a machine you can write a VHDL description of the hardware and then compile that into a C program which runs on another machine. This is how Angelo Papenhoff does it. Compare this with the top-down semantics and formal proof approach of CakeML: David MacQueen on his Ideas for Successor ML . I wonder if there is a way to combine these approaches in a kind of analytic/synthetic dialectic?  See also  How Could One Unify CMU and MIT and  Nada Amin - Metacircular Interpretation ad infinitum . Levy's book Hackers was an inspiration for these projects.   See https://pidp.net . Subscribe to Computerphile .  Here's some of the story behind these emulators: 1:14:17 New lunar lander game written three months earlier.  Subscribe to David Greelish . Mike Stewart made a gate-level emulator of the Apollo Guidance Computer and a few weeks ago he did an industrial archaeology project to find out what happened to one of the core rope memory mod...

... and physics, ... given in April 2015. Subscribe to UMD Department of Mathematics . This was given in September 2006: Subscribe to  Center for Advanced Study University of Illinois at Urbana-Champaign . The curious thing is that at the beginning of that talk he describes analogy in the same way Euclid described it (following Eudoxus) as "A is to B as C is to D" and if you write that as a ratio you get A:B = C:D. More generally you have A:B::C:D = A:C::B:D which holds for irrationals and  ἀναλογία  as well as irrationals (See Proposition 16 of Book V of Euclid's Elements ). This is analogous to Hofstadter's "Interchange" relation ( 22:35 ) he describes in the first talk above ( 14:25 ). Yesterday I was wondering about duality (see  Dual Spaces, Lie Groups and Conservation Laws ) and whether there could be any reason behind why it seems so ubiquitous in formal reasoning. I think analogy must be something fundamental in our ability to learn and interpret lan...

See  Sakara Dee at Strawberry Fair 2024  and  What is Formal Logic? Subscribe to Sakara .

This is really impressive:     Subscribe to  blargoner .   I wonder what YouTube will suggest in the auto-reply to my comment : @VisualMath  1:20 on compactness and averaging, ... and on smooth geometric structure in euclidean spaces. I have this intuition about variational calculus that I am also hoping to be able to explain once I have a nice representation of differentiable manifold, or maybe it'll work the other way around and I'll be able to get a nice representation if I follow this intuition? Maybe there's a way to find it by converging from both directions under some duality assumptions? The intuition is that in some sense the physical reason why the principle of least action works (and why Lagrange called it least action, not just stationary action) is that if we are observing some system and trying to deduce laws of motion for it, then we want to only select those paths through the configuration space which are the ones the system follows spontaneou...

See  Nada Amin - Metacircular Interpretation ad infinitum . Subscribe to Sheafification of G .

I have only just heard about this idea which goes back to the early eighties. See  Reflection and semantics in LISP  (1984) by Brian Cantwell Smith, Reification: Reflection without metaphysics  (1984) by Daniel Friedman and Mitchell Wand, Intensions and extensions in a reflective tower  (1988) by Olivier Danvy and Karoline Malmkjaer, The reflective language Black  (1996-2025) and Compiling a reflective language using MetaOCaml (2014) by Kenichi Asai. Also this summary Reflective Towers of Interpreters (2021) by Nada Amin. Scheme code at https://github.com/namin/reflective-towers. For more on Extended CPS see Abstracting control  (1990) by Olivier Danvy and Andrzej Filinski.  See also  Open, extensible object models  (2006) by Ian Piumarta and Alessandro Warth, and https://piumarta.com/software/cola/ : Programming languages often hide their implementation at a level of abstraction that is inaccessible to programmers. Decisions and trad...

He demonstrates a really slick programmable constraint solver that works from diagrams. See  On Getting Machines to do Stuff  and How Could One Unify CMU and MIT . This was held in St. Louis, Missouri.  See also  https://www.inkandswitch.com/  (and https://www.inkandswitch.com/crosscut and https://www.inkandswitch.com/untangle ).  Subscribe to Strange Loop .  8:10 On the programming model. See constraint solvers and type inference ideas in  On Getting Machines to do Stuff and  A New Kind of Science  and John Baez and Mike Stay's 2009 paper  Physics, Topology, Logic and Computation: A Rosetta Stone  and  David Jaz Maiers - Compositionality via 2-algebra . Subscribe to ACM SIGPLAN .  You can do things like this in that world too. See Thinking About How AI Can Make Better Programmers, ...   Subscribe to Dynamicland . Clemens Nylandsted Klokmose on Software as Computational Media and "Personal Digital Sovereignt...