Debian Development Reports and More

posted by Roy Schestowitz on Sep 04, 2025

• 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 an Option) 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 [...]