News for hackers. Stuff that matters.

A comment on Lean proved this program correct; then I found a bug. Parent comment

Re:Lean proved this program correct; then I found a bug by gopiandcode on Monday April 13, 2026 @11:33PM (#47760941)
It does seem that way doesn't it? But as software bugs are becoming easier to find and exploit, I'm expecting more and more people, including those not "sophisticated enough" to understand and employ formal verification to start using it
[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by quantummagic on Tuesday April 14, 2026 @12:33AM (#47761279)
> I'm expecting more and more people

Then it would help to not introduce any confusion into the ecosystem by using a click-baity title that implies you found a bug which violated the formal specification.

[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by sn9 on Tuesday April 14, 2026 @06:43PM (#47772413)
We should not cater to people who make decisions based on titles instead of reading the actual article.
[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by quantummagic on Tuesday April 14, 2026 @10:21PM (#47773916)
That's a shitty rationale for click-bait titles. Good titles are for the benefit of people who actually read the articles too.
[ Parent | on HN ]