The readings shared in Bluesky on 3 September 2025 are

• Thinking programs (Logical modeling and reasoning about languages, data, computations, and executions). ~ Wolfgang Schreiner. #ITP #IsabelleHOL #Logic #CompSci
• A blueprint for the formalization of Carleson's theorem on convergence of Fourier series. ~ Lars Becker et als. #ITP #LeanProver #Math
• Lean for JavaScript developers. ~ Dan Abramov. #ITP #LeanProver
• Contradiction, contraposition and Lean. ~ Oussama. #ITP #LeanProver
• The meta-principle: A type-theoretic theorem and its interpretation. ~ Jonathan Washburn. #ITP #LeanProver
• Introduction to formal methods using interactive proof assistant Rocq. ~ Evgeny Makarov. #ITP #Rocq
• #Exercitium: Entero positivo de la cadena. #Haskell #ProgramaciónFuncional #Matemáticas