The readings shared in Bluesky on 11 April 2025 are

• Code generation via meta-programming in dependently typed proof assistants. ~ Mathis Bouverot-Dupuis, Yannick Forster. #ITP #Agda #Rocq #LeanProver
• A comparative review of ZFC, NBG, and MK axiom systems: Theoretical foundations and formalization in Coq. ~ Si Chen, Wensheng Yu. #ITP #Coq #Rocq #Math #SetTheory
• A (very niche) footgun in GHC.Generics. ~ welltypedwitch. #Haskell #FunctionalProgramming
• Refactoring strings in GHC. ~ Brandon Chinn. #Hakell #FunctionalProgramming
• #Exercitium: Código de las alergias. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[f⁻¹[u]​] ⊆ u". #LeanProver #IsabelleHOL #Math