Remix.run Logo
▲ turbobutton 3 hours ago

Having 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.

▲i_am_a_peasant 3 hours ago | parent | next [-]

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.

▲bajard 2 hours ago | parent [-]

I once had a sensor that rounded the data, so the output unwittingly fitted into a grid. The equations that had to be used on that data gave infinite results because the grid sometimes rounded slopes into vertical lines.

So I had to reconstruct a signal that fitted the data for the equations to work at all. But the reconstruction was no longer measured data. It was made up, and there was no single solution for fitting the data. That meant I could claim to "respect the data" while producing any result I wanted.

▲i_am_a_peasant 2 hours ago | parent [-]

Reminds me of that von Neumann quote "With four parameters I can fit an elephant, and with five I can make him wiggle his trunk."

▲aleph_minus_one 21 minutes ago | parent [-]

> "With four parameters I can fit an elephant, and with five I can make him wiggle his trunk."

Indeed: here are two papers on this topic:

Jürgen Mayer; Khaled Khairy; Jonathon Howard. Drawing an elephant with four complex parameters. 2010. https://pubs.aip.org/aapt/ajp/article-abstract/78/6/648/1042... Article without paywall : https://publications.mpi-cbg.de/Mayer_2010_4314.pdf

Dian Jin; Junze Yuan. Fitting an Elephant with Four non-Zero Parameters. 2024. https://arxiv.org/abs/2407.07909v1

▲perching_aix 3 hours ago | parent | prev [-]

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