The microblog: 2023.08.11 20:36:50

2023.08.11 20:36:50 (Mastodon 110872901089898818, Twitter 1690099906202206213) from Daniel J. Bernstein:

Now posted HOL Light formalizations of the same theorems about decoding Goppa codes: ( via Cloudflare). More verbose than the Lean versions, but took me less time to write. Which will be a better foundation for software verification?