During the days I was studying/working with Coq, one visiting professor gave a presentation on defense software design. An example presented was control logic for F-16, which the professor presumably worked on. A student asked how do you prove "correctness", i.e. operability, of a jet fighter and its control logic? I don't think the professor had a satisfying answer.

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.

▲

dwohnitmok 5 hours ago | parent | next [-]

You use floating point numbers instead of real numbers in your theorems and function definitions.

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)

▲

quanto 4 hours ago | parent | next [-]

> when I can get away with it I'd prefer to prove things with real numbers and assume magically they transfer to floating point.

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?

	▲	thesmtsolver 4 hours ago \| parent \| next [-]
		There is nothing inherently difficult about practical implementations of continuous numbers for automated reasoning compared to more discrete mathematical structures. They are handleable by standard FOL itself. 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://smt-lib.org/theories-Reals.shtml
	▲	kragen 4 hours ago \| parent \| prev [-]
		I'm curious about how you'd do that, too. I haven't tried doing anything like that, but I'd think you'd start by trying to formalize the usual optimality proof for the Kalman filter, transfer it to actual program logic on the assumption that the program manipulates real numbers, try to get the proof to work on floating-point numbers, and finally extract the program from the proof to run it. https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization.

▲

anthk an hour ago | parent | prev [-]

You use reducing rationals everywhere you can, not floast.

▲

tensegrist 4 hours ago | parent | prev [-]

> There are documented tragedies where numerical rounding error of the control logic of a missile costed lives.

curious about this

	▲	codenaught 3 hours ago \| parent [-]
		This is likely a reference to the Patriot missile rounding issue that arguably led to 28 deaths. https://www-users.cse.umn.edu/~arnold/disasters/Patriot-dhar... https://www.gao.gov/assets/imtec-92-26.pdf