Articles for general-audience viewing, some targeted at a more niche audience than others 𒊑𒀀 / 𒊑𒅀 What machines can and can't do An opinionated history of programming languages 2043 — a short story Predicativity in Coq Equality in Mechanized Mathematics An inquiry into the Foundations of Mathematics ZFC and propositional logic Lean versus Coq: The cultural chasm