My question is the same, albeit more technically refined. How do you prove the correctness of a numerical algorithm (operating on a quantized continuum) using type-theoretic/category-theoretic tools like theorem provers like Coq? There are documented tragedies where numerical rounding error of the control logic of a missile costed lives. I have proved mathematical theorems before (Curry-Howard!) but they were mathematical object driven (e.g. sets, groups) not continuous numbers.
This sounds flippant, but I'm being entirely earnest. It's a significantly larger pain because floating point numbers have some messy behavior, but the essential steps remain the same. I've proved theorems about floating point numbers, not reals. Although, again, it's a huge pain, and when I can get away with it I'd prefer to prove things with real numbers and assume magically they transfer to floating point. But if the situation demands it and you have the time and energy, it's perfectly fine to use Coq/Rocq or any other theorem prover to prove things directly about floating point arithmetic.
The article itself is talking about an approach sufficiently low level that you would be proving things about floating point numbers because you would have to be since it's all assembly!
But even at a higher level you can have theorems about floating point numbers. E.g. https://flocq.gitlabpages.inria.fr/
There's nothing category theoretic or even type theoretic about the entities you are trying to prove with the theorem prover. Type theory is merely the "implementation language" of the prover. (And even if there was there's nothing tying type theory or category theory to the real numbers and not to floats)
IEE754 does a good job explaining the representation, but it doesn't define all the operations and possible error codes as near as I can tell.
Is it just assumed "closest representable number to the real value" always?
What about all the various error codes?
True for some approaches, but numerical analysis does account for machine epsilon and truncation errors.
I am aware that Inria works with Coq as your link shows. However, the link itself does not answer my question. As a concrete example, how would you prove an implementation of a Kalman filter is correct?
See ACL2's support for floating point arithmetic.
https://www.cs.utexas.edu/~moore/publications/double-float.p...
SMT solvers also support real number theories:
https://shemesh.larc.nasa.gov/fm/papers/nfm2019-draft.pdf
Z3 also supports real theories:
https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization.
curious about this
https://www-users.cse.umn.edu/~arnold/disasters/Patriot-dhar...
The Patriot missile didn’t kill 28 people accidentally, it simply failed to intercept an enemy missile.
And it wasn’t launched on an incorrect trajectory either, the radar was looking at a slightly wrong distance window and lost track. Furthermore, the error only starts having an effect after 100 hours of operation, and it seems to have only been problematic with the faster missiles in Iraq that the system wasn’t designed for. They rushed the update and they did actually write a function to deal with this exact numerical issue, but during the refactor they missed one place where it should have been used.
28 lives are obviously significant, but just to note that there are many mitigating factors.
ACL2 is also VERY powerful and capable.
In this end, it is all about the complexity and stability in time for this matter.
I wonder if AI's compute graph would benefit from a language-level rigor as of Coq.
I'm no expert on assembly-language programming, but probably 90% of the assembly I write on i386, amd64, RISC-V, and ARM is about 40 instructions: ldr, mov, bl, cmp, movs, push, pop, add, b/jmp, bl/blx/call, ret, str, beq/jz, bne/jnz, bhi/ja, bge/jge, cbz, stmia, ldmia, ldmdb, add/adds, addi, sub/subs, bx, xor/eor, and, or/orr, lsls/shl, lsrs/sar/shr, test/tst, inc, dec, lea, and slt, I think. Every once in a while you need a mul or a div or something. But the other 99% of the instruction set is either for optimized vectorized inner loops or for writing operating system kernels.
I think that the reason that i386 assembly (or amd64 assembly) is error-prone is something else, something it has in common with very simple architectures and instruction sets like that of the PDP-8.
What reason is that? (And, if it's not obvious, what are ARM/RISC-V doing that make them less bad?)
There are various minor details of one architecture or the other that make them more or less bug-prone, but those are minor compared to what they have in common.
None of this is because the instruction sets are complex. It would be closer to the mark to say that it's because they are simple.
I've not fleshed this out yet, but I think a relatively simple system would help deal with all the issues you mention in the first paragraph while allowing escape hatches.
Renaming languages to suit American taste really grates.
Nimrod to Nim was even worse. Apparently Americans cannot get Biblical references.