news
Debian Development Reports and More
-
Joachim Breitner: F91 in Lean
Back in March, with version 4.17.0, Lean introduced
partial_fixpoint
, a new way to define recursive functions. I had drafted a blog post for the official Lean FRO blog back then, but forgot about it, and with the Lean FRO blog discontinued, I’ll just publish it here, better late than never.With the
partial_fixpoint
mechanism we can model possibly partial functions (so those returning anOption
) without an explicit termination proof, and still prove facts about them. See the corresponding section in the reference manual for more details.On the Lean Zulip, I was asked if we can use this feature to define the McCarthy 91 function and prove it to be total. This function is a well-known tricky case for termination proofs.
-
Paul Wise: FLOSS Activities August 2025
-
Enrico Zini: CAdES signatures on Debian
CAdES is a digital signature standard that is used and sometimes mandated, by the Italian Public Administration.
To be able to do my job, I own a Carta Nazionale dei Servizi (CNS) with which I can generate legally binding signatures. Now comes the problem of finding a software to do it.
-
Chiark ☛ Colin Watson: Free software activity in August 2025
About 95% of my Debian contributions this month were [...]