> However, the complexity of the algorithms, and, in particular, the presence of various special cases in the code which occur with very low but non-zero probability make it impossible to rule out the possibility of bugs remaining in the program.

Sounds like perhaps a nice testcase for formalization + AI?

▲

5 hours ago | parent | next [-]

[deleted]

▲

teiferer 6 hours ago | parent | prev [-]

It's beyond me why such foundational libraries don't have formal correctness proofs attached these days.

	▲	winwang 4 hours ago \| parent [-]
		imo, partially because it's still not easy (in terms of code -> formal proof). With AI, I've been Lean-ifying a simpler (but non-trivial) algo. Pointing (current) AI at it only goes so far and in fact might go "too far" in certain cases, where a non-formalized argument would have sufficed. There's also "who watches the watcher" -- did it really prove what we're supposed to prove? For something like these compression algos, though, I imagine it would be much easier since they already have actual proofs out there.