alt Hacker NewsHaving been downvoted, I like to clarify that this comes from the experience working in finance with developers with a strong academic background that emphasized on the necessity of formal proof to a point where complexity made actual progress nearly impossible- while simultaneously basing the proof repeatedly on assumptions that did not uphold in practice.
Replies
perching_aix • today at 12:08 PM
what were some categories of such assumptions, can you name some examples?
a fun one that immediately comes to mind is asserting something holds for reals, but not evaluating whether it holds for IEEE floats, though maybe that's not really a thing in finance due to rounding related rules anyways
Nah I don't disagree with you. Thing is even if you formally prove that for every input you produce a valid output. In safety certified software, there's the problem that if that input comes from a sensor, a sensor is an inherently probabilistic thing, and it may be that you will have false positives. The best you can do is build a safety case that even if you get false positives you end up in a safe state, but you can't guarantee that they won't ever increase operational costs.