The readings shared in Bluesky on 2 November 2025 are:

• "Why don't you use dependent types?" ~ Lawrence Paulson. #ITP #Automath #LCF #IsabelleHOL #LeanProver #TypeTheory
• Lean4Physics: Comprehensive reasoning framework for college-level Physics in Lean4. ~ Yuxin Li et als. #ITP #LeanProver #Physics #AI #LLM
• On graded coeffect types for information-flow control. ~ Vilem-Benjamin Liepelt et als. #ITP #Agda
• Property-based testing for asynchronous functional reactive programming using linear temporal logic. ~ Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr. #Haskell #FunctionalProgramming