7 ms·

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

by quanto 10mo ago

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 10mo ago
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/ 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 10mo ago
  > 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 10mo ago
    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.pdf 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 https://shemesh.larc.nasa.gov/fm/papers/nfm2019-draft.pdf Z3 also supports real theories: https://smt-lib.org/theories-Reals.shtml https://smt-lib.org/theories-Reals.shtml
  - kragen 10mo ago
    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 https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization.
    - thesmtsolver 10mo ago
      It is really not that difficult. Here is a paper that formalizes a version of feed forward networks to prove properties about them. https://arxiv.org/pdf/2304.10558 https://arxiv.org/pdf/2304.10558
- anthk 10mo ago
  You use reducing rationals everywhere you can, not floast.
  - dwohnitmok 10mo ago
    This is potentially horrendous for performance, and even worse, unpredictably so. Instead of getting the incorrect answer (or NaN) with floating point if you have an unfortunate series of calculations, you get extreme memory blowup, where your numerator and denominator can explode in size, which in turn leads to runtime slowdown. In the worst case you can actually run out of memory (because certain fairly natural calculations can cause your numerators and denominators to very rapidly explode in size). Committing to unbounded rationals basically opens your system up to DoS attacks. You could decide to bound rationals in the numerator and denominator, but then you've more or less reinvented a form of floating point. In order of preference for a high reliability production system I would use: 1. Integers 2. Fixed point 3. Floating point 4. Rationals [waaaayyyy down in fourth place] Most systems don't have high enough reliability needs though that I would favor fixed point over floating point and so in practice I rarely use fixed point (simply because library and language support is far worse).
    - anthk 10mo ago
      Most people versed in fixed point (microcontroller programmers, Forth programmers) will use rationals at decent speeds because they know all the tricks for performance, kinda like HAKMEM algos applied to Forth instead of a PDP10 (and OFC the Forth Scientific Library). https://www.inwap.com/pdp10/hbaker/hakmem/hakmem.html https://www.inwap.com/pdp10/hbaker/hakmem/hakmem.html Edit: link
      - dwohnitmok 10mo ago
        I don't see anywhere in HAKMEM where they advocate for the use of unbounded rational numbers. Do you have any examples of unbounded rational numbers used in a microcontroller program, in a production Forth program, or really in any production user-facing codebase? I ask specifically for unbounded rational numbers because again bounded rational numbers are effectively equivalent to floating point and fixed denominator rational numbers are equivalent to fixed point.
- grumpymuppet 10mo ago
  I have been curious about this. Where can you find definitions for the basic operations to build up from? 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?
  - adrian_b 10mo ago
    The standardized operations, e.g. multiplication or square root extraction, are precisely defined, i.e. the result is always defined exactly, by the combination of the corresponding operation with real numbers and by the rounding rule that is applied. IEEE 754 also contains a list of operations that are recommended, but not defined by the standard, such as the exponential function and other functions where it is difficult to round exactly the result. For the standardized operations, all the possible errors are precisely defined and they must either generate an appropriate exception or produce as result a special value that encodes the kind of error, depending on how the programmer configures the processor. The standard is perfectly fine. The support of the standard in the popular programming languages is frequently inconvenient or only partial or even absent. For instance it may be impossible to choose to handle the errors by separate exception handlers and it may be impossible to unmask some of the exceptions that are masked by default. Or you may lack the means to control the rounding mode or to choose when to use FMA operations and when to use separate multiplications. If you enable all the possible exceptions, including that for inexact results, the value of an expression computed with IEEE 754 operations is the same as if it were computed with real numbers, so you do not need to prove anything extra about it. However this is seldom helpful, because most operations with FP numbers produce inexact results. If you mask only the exception for inexact results, the active rounding rule will be applied after any operation that produces an inexact result. Then the expression where you replace the real numbers with FP numbers is equivalent with a more complex expression with real numbers that contains rounding operations besides the explicit operations. Then you have to prove whatever properties are of interest for you when using the more complex expression, which includes rounding operations. The main advantage of the IEEE 754 standard in comparison with the pathetic way of implementing FP operations before this standard, is that the rounding operations are defined exactly, so you can use them in a formal proof. Before this standard, most computer makers rounded the results in whatever way happened to be cheaper to implement and there were no guarantees about which will be the result of an operation after rounding, so it was impossible to prove anything about FP expressions computed in such computers. If you want to prove something about the computation of an expression when more exceptions are masked, not only the inexact result exception, that becomes more complex. When a CPU allows a non-standard handling of the masked exceptions, like flush-to-zero on underflow, that can break any proof.
tensegrist 10mo ago
> There are documented tragedies where numerical rounding error of the control logic of a missile costed lives. curious about this
- codenaught 10mo ago
  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-dharan-skeel-siam.pdf https://www-users.cse.umn.edu/~arnold/disasters/Patriot-dhar... https://www.gao.gov/assets/imtec-92-26.pdf https://www.gao.gov/assets/imtec-92-26.pdf
  - oersted 10mo ago
    Just to clarify for others because it’s a tiny bit clickbaity: 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.
OneDeuxTriSeiGo 10mo ago
So the answer is that you are proving two things: 1. That the model/specification makes sense. i.e. that certain properties in the model hold and that it does what you expect. 2. That the SUV/SUT (system under verification/test) corresponds to the model. This encompasses a lot but really what you are doing here is establishing how your system interacts with the world, with what accuracy it does so, etc. And from there you are walking along the internal logic of your system and mapping your representations of the data and the algorithms you are using into some projection from the model with a specified error bound. So you are inherently dealing with the discrete nature of the system the entire time but you can reason about that discrete value as some distribution of possible values that you carry through the system with each step either - introducing some additional amount of error/variability or - tightening the bound of error/variability but trapping outside values into predictable edge cases. Then it's a matter of reasoning about those edge cases and whether they break the usefulness of the system compared against the idealised model.
auggierose 10mo ago
Curry-Howard is not needed for theorem proving, it's just that type theorists like it. See https://www.cl.cam.ac.uk/~jrh13/papers/thesis.html https://www.cl.cam.ac.uk/~jrh13/papers/thesis.html for your question, John Harrison got a job with Intel based on this after their floating point disaster. But in short: theorem proving is not about equalities, it is about inequalities. And theorems about numerical algorithms are a great example of this.

by quanto 10mo ago

dwohnitmok 10mo ago

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/ 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 10mo ago
> 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 10mo ago
  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.pdf 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 https://shemesh.larc.nasa.gov/fm/papers/nfm2019-draft.pdf Z3 also supports real theories: https://smt-lib.org/theories-Reals.shtml https://smt-lib.org/theories-Reals.shtml
- kragen 10mo ago
  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 https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization.
  - thesmtsolver 10mo ago
    It is really not that difficult. Here is a paper that formalizes a version of feed forward networks to prove properties about them. https://arxiv.org/pdf/2304.10558 https://arxiv.org/pdf/2304.10558
anthk 10mo ago
You use reducing rationals everywhere you can, not floast.
- dwohnitmok 10mo ago
  This is potentially horrendous for performance, and even worse, unpredictably so. Instead of getting the incorrect answer (or NaN) with floating point if you have an unfortunate series of calculations, you get extreme memory blowup, where your numerator and denominator can explode in size, which in turn leads to runtime slowdown. In the worst case you can actually run out of memory (because certain fairly natural calculations can cause your numerators and denominators to very rapidly explode in size). Committing to unbounded rationals basically opens your system up to DoS attacks. You could decide to bound rationals in the numerator and denominator, but then you've more or less reinvented a form of floating point. In order of preference for a high reliability production system I would use: 1. Integers 2. Fixed point 3. Floating point 4. Rationals [waaaayyyy down in fourth place] Most systems don't have high enough reliability needs though that I would favor fixed point over floating point and so in practice I rarely use fixed point (simply because library and language support is far worse).
  - anthk 10mo ago
    Most people versed in fixed point (microcontroller programmers, Forth programmers) will use rationals at decent speeds because they know all the tricks for performance, kinda like HAKMEM algos applied to Forth instead of a PDP10 (and OFC the Forth Scientific Library). https://www.inwap.com/pdp10/hbaker/hakmem/hakmem.html https://www.inwap.com/pdp10/hbaker/hakmem/hakmem.html Edit: link
    - dwohnitmok 10mo ago
      I don't see anywhere in HAKMEM where they advocate for the use of unbounded rational numbers. Do you have any examples of unbounded rational numbers used in a microcontroller program, in a production Forth program, or really in any production user-facing codebase? I ask specifically for unbounded rational numbers because again bounded rational numbers are effectively equivalent to floating point and fixed denominator rational numbers are equivalent to fixed point.
grumpymuppet 10mo ago
I have been curious about this. Where can you find definitions for the basic operations to build up from? 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?
- adrian_b 10mo ago
  The standardized operations, e.g. multiplication or square root extraction, are precisely defined, i.e. the result is always defined exactly, by the combination of the corresponding operation with real numbers and by the rounding rule that is applied. IEEE 754 also contains a list of operations that are recommended, but not defined by the standard, such as the exponential function and other functions where it is difficult to round exactly the result. For the standardized operations, all the possible errors are precisely defined and they must either generate an appropriate exception or produce as result a special value that encodes the kind of error, depending on how the programmer configures the processor. The standard is perfectly fine. The support of the standard in the popular programming languages is frequently inconvenient or only partial or even absent. For instance it may be impossible to choose to handle the errors by separate exception handlers and it may be impossible to unmask some of the exceptions that are masked by default. Or you may lack the means to control the rounding mode or to choose when to use FMA operations and when to use separate multiplications. If you enable all the possible exceptions, including that for inexact results, the value of an expression computed with IEEE 754 operations is the same as if it were computed with real numbers, so you do not need to prove anything extra about it. However this is seldom helpful, because most operations with FP numbers produce inexact results. If you mask only the exception for inexact results, the active rounding rule will be applied after any operation that produces an inexact result. Then the expression where you replace the real numbers with FP numbers is equivalent with a more complex expression with real numbers that contains rounding operations besides the explicit operations. Then you have to prove whatever properties are of interest for you when using the more complex expression, which includes rounding operations. The main advantage of the IEEE 754 standard in comparison with the pathetic way of implementing FP operations before this standard, is that the rounding operations are defined exactly, so you can use them in a formal proof. Before this standard, most computer makers rounded the results in whatever way happened to be cheaper to implement and there were no guarantees about which will be the result of an operation after rounding, so it was impossible to prove anything about FP expressions computed in such computers. If you want to prove something about the computation of an expression when more exceptions are masked, not only the inexact result exception, that becomes more complex. When a CPU allows a non-standard handling of the masked exceptions, like flush-to-zero on underflow, that can break any proof.

tensegrist 10mo ago

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

codenaught 10mo ago
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-dharan-skeel-siam.pdf https://www-users.cse.umn.edu/~arnold/disasters/Patriot-dhar... https://www.gao.gov/assets/imtec-92-26.pdf https://www.gao.gov/assets/imtec-92-26.pdf
- oersted 10mo ago
  Just to clarify for others because it’s a tiny bit clickbaity: 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.

OneDeuxTriSeiGo 10mo ago

So the answer is that you are proving two things: 1. That the model/specification makes sense. i.e. that certain properties in the model hold and that it does what you expect. 2. That the SUV/SUT (system under verification/test) corresponds to the model. This encompasses a lot but really what you are doing here is establishing how your system interacts with the world, with what accuracy it does so, etc. And from there you are walking along the internal logic of your system and mapping your representations of the data and the algorithms you are using into some projection from the model with a specified error bound. So you are inherently dealing with the discrete nature of the system the entire time but you can reason about that discrete value as some distribution of possible values that you carry through the system with each step either - introducing some additional amount of error/variability or - tightening the bound of error/variability but trapping outside values into predictable edge cases. Then it's a matter of reasoning about those edge cases and whether they break the usefulness of the system compared against the idealised model.

auggierose 10mo ago

Curry-Howard is not needed for theorem proving, it's just that type theorists like it. See https://www.cl.cam.ac.uk/~jrh13/papers/thesis.html https://www.cl.cam.ac.uk/~jrh13/papers/thesis.html for your question, John Harrison got a job with Intel based on this after their floating point disaster. But in short: theorem proving is not about equalities, it is about inequalities. And theorems about numerical algorithms are a great example of this.