News for hackers. Stuff that matters.
Re:The Mathocalypse by mrob on Thursday October 08, 2026 @04:20AM (#50003182)
>A maths theorem that can only be partially understood/proven only has value as marketing collateral.

There are many problems that aren't "interesting" in a mathematical sense but can still have valuable proofs. The entire field of formal methods in software development is mostly about this kind of problem. If I want to be sure that no input can cause out-of-bounds memory access, or that my superoptimizer found the lowest possible cycle count, I don't care if it's elegant, I just need some machine-readable proof I can run through my trusted verifier.

Re:The Mathocalypse by Tanjreeve on Thursday October 08, 2026 @01:03PM (#50008496)
When we use verification to build software. We have an actual software as an output and hopefully some sort of problem solvsd the verification is also not in an of itself valuable.
Re:The Mathocalypse by mrob on Thursday October 08, 2026 @01:25PM (#50008845)
The verification itself is valuable because it gives us confidence that the software is correct. This knowledge changes what we do with the software. E.g. do we need to sandbox it before processing untrusted inputs? Is it safe to put it on a hostile network? Can we use it to control an airplane or a nuclear reactor? Even if the code remains identical, formally verifying software improves it because it lets us use it in situations where unverified software would be too risky.