Formalizing Julia in Lean (and finding 400+ bugs in Base)

Formalizing Julia in Lean Not sure how much people have been following the ongoing cybersecurity apocalypse, but one of the interesting things I’ve learned from it is how exactly teams have been finding exploits. Some of these exploits are found by formalizing software into Lean 4, and then attempting to prove (or refute) rigorously that certain properties are respected. This can identify problems that even the most heavy-handed prop-testing can fail to catch. Before AI coding agents, this wo...