This is the #Lean 4 #proof of the nonexistence of #God, based on "§2.4 Modeling English Propositions" p.37 of "A Logical Approach to Discrete Mathematics" by Gries and Schneider (1993):

• If God were able and willing to prevent evil, He would do so:
Able ∧ Willing → Prevents
• If God were unable to prevent evil, He would be impotent:
¬Able → Impotent
• If God were unwilling to prevent evil, He would be malevolent:
¬Willing → Malevolent
• God does not prevent evil:
¬Prevents
• If God exists, He is neither impotent nor malevolent:
GodExists → ¬Impotent ∧ ¬Malevolent
• Therefore, God does not exist:
¬GodExists

Shed no tears for me, were I to end up in #Hell. That my code type checks in Lean 4 at all is a little bit of #Heaven for me.

#DependentTypes #ProofAssistants

https://shorturl.at/wbp1V

This is the #Lean 4 #proof of the nonexistence of #God, based on "§2.4 Modeling English Propositions" p.37 of "A Logical Approach to Discrete Mathematics" by Gries and Schneider (1993):

• If God were able and willing to prevent evil, He would do so:
Able ∧ Willing → Prevents
• If God were unable to prevent evil, He would be impotent:
¬Able → Impotent
• If God were unwilling to prevent evil, He would be malevolent:
¬Willing → Malevolent
• God does not prevent evil:
¬Prevents
• If God exists, He is neither impotent nor malevolent:
GodExists → ¬Impotent ∧ ¬Malevolent
• Therefore, God does not exist:
¬GodExists

Shed no tears for me, were I to end up in #Hell. That my code type checks in Lean 4 at all is a little bit of #Heaven for me.

#DependentTypes #ProofAssistants

https://shorturl.at/wbp1V

The Agda standard library has been published in the Journal of Open Source Software. Congratulations to Matthew Daggitt, @gallais , James McKinna, Andreas Abel, @Taneb , @mudri , Ulf Norell, @oisdk, Sergei Meshveliani, Sandro Stucki, @JacquesC2, Alex Rice, Jason Hu, Li-yao Xia, Shu-Hung You, @totbwf and @wen !

joss.theoj.org/papers/10.21105/joss.09241

#Agda #ITP #DependentTypes #JOSS #OSS

The Agda standard library has been published in the Journal of Open Source Software. Congratulations to Matthew Daggitt, @gallais , James McKinna, Andreas Abel, @Taneb , @mudri , Ulf Norell, @oisdk, Sergei Meshveliani, Sandro Stucki, @JacquesC2, Alex Rice, Jason Hu, Li-yao Xia, Shu-Hung You, @totbwf and @wen !

joss.theoj.org/papers/10.21105/joss.09241

#Agda #ITP #DependentTypes #JOSS #OSS

Dependent types and how to get rid of them

https://chadnauseam.com/coding/pltd/are-dependent-types-actually-erased

#HackerNews #DependentTypes #Erasure #Coding #SoftwareDevelopment #Programming #LanguageTheory #HackerNews

"Why don't you use dependent types?"

https://lawrencecpaulson.github.io//2025/11/02/Why-not-dependent.html

#HackerNews #dependenttypes #programming #philosophy #typeTheory #HN #discussion #HackerNews

Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!

The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!

Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!

#Agda#ProofAssistants#DependentTypes#Angers

Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!

The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!

Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!

#Agda#ProofAssistants#DependentTypes#Angers