The Eternal Doorman

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.  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: Programming languages often hide their implementation at a level of abstraction that is inaccessible to programmers. Decisions and tradeoffs made by the language designer at this level (single vs. multiple inheritance, mixins vs. T...

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...

I found this talk by accident, on William Byrd's web page . It was given at Stanford in March 2013 whilst I was living in Rurrenabaque trying in vain to sell my logic books to get some money to buy food. See the book  Surfaces and Essences Analogy as the Fuel and Fire of Thinking . Subscribe to ccrmalite  (?!). There used to be a distinction between symbolic logic and formal logic. If you ask Google AI what this distinction is it says it is no longer, since formal logic before 1900 was found to be wanting in rigour and thanks to the efforts of Frege, Russell et al it has been superseded by symbolic logic. Well, if Google AI says that then it must be true. What if Frege, Russell et al  had actually not properly understood what formal logic was? Then there would be a distinction between Formal Logic and modern symbolic logic which is unknowable to anyone who only recognises modern symbolic logic. In fact you don't have to look very far to see that this is clearly the case...

See this 2020 paper Gentzen-Mints-Zucker duality by Daniel Murfet and William Troiani: The Curry-Howard correspondence is often described as relating proofs (in intutionistic natural deduction) to programs (terms in simply-typed lambda calculus). However this narrative is hardly a perfect fit, due to the computational content of cut-elimination and the logical origins of lambda calculus. We revisit Howard's work and interpret it as an isomorphism between a category of proofs in intuitionistic sequent calculus and a category of terms in simply-typed lambda calculus. In our telling of the story the fundamental duality is not between proofs and programs but between local (sequent calculus) and global (lambda calculus or natural deduction) points of view on a common logico-computational mathematical structure.  See also  Program Synthesis and  On Getting Machines to do Stuff  and then  Jean-Yves Girard - Lectures at IHP thematic trimester : Semantics of proofs and...

See  https://freenet.org . See  Polylog on Oblivious Transfer and Zero Knowledge Protocols  and  HTML in Blog Posts . See also  Taylor and Amy Experiment With an Open Source, Decentralised, Encrypted Way to Message Complete Strangers . For the background, see  Ian Clarke on Freenet  and  Ian Clarke Answering Questions About Freenet . Subscribe to FUTO .     Subscribe to FUTO .  

See  https://github.com/dmacqueen/NewFrontEnd  and  https://standardml.zulipchat.com . 9:33 On disallowing static declarations within expressions: from MLFW2025.txt : 1.3. [Core] No static (type/module) declarations within expressions   Moto: "Keep the core and module levels separate", or "no static declarations within   dynamic expressions".   What does it, or should it, mean to have a (statically generative) datatype declaration   in the body of a recursive function.   [Karl Crary (and Bob Harper?) won't like this, since definition of modules within   expressions is a feature of his dialect of (S)ML. It also appears to be supported in   Moscow ML. The CMU (Harper, Crary, etc.) view of the static semanatics of (S)ML seems to   base on some fundamental "type theoretic" notion of a _module_ that seems to be   different from my own intuitive understanding of the module system of (S)ML. Their ideas   are described in papers s...

I just found out that POPL 2024 had some talks about program synthesis. This reminded me of the Criterion Problem. See  Ways to Do Telecommunications : Subscribe to ACM SIGPLAN .

This is great! See Hackaday Europe 2026: Half Quad, Half Blimp: Test. Fly. Survive . Subscribe to Hackaday .

See  Jean-Yves Girard - Lectures at IHP thematic trimester : Semantics of proofs and certified mathematics  for more charcuterie. It's where the sausages are all hanging up around the ceiling, ... Subscribe to Julie Nolke .