The Eternal Doorman

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 .  

My comment : That was a really clear explanation, thank you. Can you talk sometime about how it is that these protocols are not used for basic data protection? I mean why is age verification such a big deal? Can't a zero knowledge protocol be used to verify someone's age without divulging their full identity? I know there is probably a different motive behind the age verification thing, but why does nobody talk about alternative solutions that don't involve personal identity data? I think it has much wider application though. For example, say I want to order and pay for something and have it delivered to me without divulging my identity or the delivery address or my bank details. One would think that it would be possible for my bank to give me some proof that I have commited to pay a certain amount to some entity, a sort of single use cheque, which I could then commit to using to pay the supplier, who then commits to send the goods via a chain of carriers who each similary ...