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: https://cr.yp.to/2023/lightgoppa-20230811-verify.html (https://cr-yp-to.viacache.net/2023/lightgoppa-20230811-verify.html via Cloudflare). More verbose than the Lean versions, but took me less time to write. Which will be a better foundation for software verification?