[vanderZwan]

Well, the examples so do fall more under the abstractly provable side of things when it comes to their behavior.

But take the Sieve algorithm that was posted yesterday[0], or Powersort[1] (Timsort with its bugs fixed). To some degree those are more engineering discoveries about which algorithm behaves best with real-world data. Although Powersort actually involves a lot of formal maths to prove it does not have degenerate edge-cases, so maybe I should have stuck with Timsort.

[0] https://news.ycombinator.com/item?id=38850202

[1] https://www.wild-inter.net/publications/munro-wild-2018