4 ms·

Still, I don't think you can use it to avoid (physical) crashes due to an incorrect algorithm, simply because theorem provers work on a cognitive basis but cont

Still, I don't think you can use it to avoid (physical) crashes due to an incorrect algorithm, simply because theorem provers work on a cognitive basis but control systems operate on continuous fields (i.e. transfer functions defined over the complex numbers).

tom_mellior 10y ago
Believe it or not, people working on theorem proving are aware that computers use finite arithmetic, and they take this into account. Yes, floating-point computations are hard and painful to verify. But no, it's not that easy to hand-wave away the whole field :-)
- aseipp 10y ago
  Honestly, it seems floating point computations are, by some measure, possibly pretty old at this point in the formal methods world! Intel has been investing in formal verification of its floating point units since at least the 90s when FDIV hit them, and this was when the tech was way worse than what we have today! Hell, CompCert -- which you can download today -- already has a proven adherence to IEEE-754 floating point, implemented by specifying IEEE-754 semantics in Coq, then using that to create a proof the compiler correctly preserves the semantics of IEEE-754 during the compilation process.
aseipp 10y ago
People doing theorem proving and formal methods know what complex numbers are, I can assure you. Mathematicians have plenty of statements about the properties of complex numbers, and many theorem provers have libraries that even formalize those statements and proofs in mechanized, automated ways that can be trusted. I'm not sure how "complex numbers are involved" is any more of a mystical problem than "finite-field arithmetic is involved" is a problem: it isn't. I think I get what you mean, though. No, you cannot prove "my drone is magical and awesome and will never crash land even if I tell it to, and it takes the best pictures of any drone". You cannot mathematically prove "My on-board sensor will always work and defy the laws of physics and never be inaccurate". You CAN mathematically prove "My drone control software never reaches an illegitimate state, that would cause the system to deadlock or hang due to a software error, making the drone crash in a possibly dangerous, uncontrolled way". You CAN prove "My software will respond within exactly N cycles, at most, to any external incoming sensor signal". That kind of guarantee is extremely valuable for such systems. It isn't easy (and requires deep, conjoined assumptions and proofs of both the hardware and software), but it's hardly impossible. And sure, there is only so much the model can prove to you, at some point it has to exist "in the real world". This isn't really a counter-point to the actual formal methods field, though. To couch it in a more concrete example: when people like Intel say "our CPUs don't catch on fire", they only mean it in a very specific sense. Sure, you can shove newspaper up next to your heatsink, and then when it catches on fire say "See! You were wrong!" But the reality is that their statement is sort of couched in the assumption that, well, you aren't going to do that. It's fairly reasonable to assume some limitations of your model. But this really has very little to do with being able to formalize general mathematics (like complex numbers or finite fields or N-dimensional spaces) using a theorem prover, or whatever.

tom_mellior 10y ago

Believe it or not, people working on theorem proving are aware that computers use finite arithmetic, and they take this into account. Yes, floating-point computations are hard and painful to verify. But no, it's not that easy to hand-wave away the whole field :-)

aseipp 10y ago
Honestly, it seems floating point computations are, by some measure, possibly pretty old at this point in the formal methods world! Intel has been investing in formal verification of its floating point units since at least the 90s when FDIV hit them, and this was when the tech was way worse than what we have today! Hell, CompCert -- which you can download today -- already has a proven adherence to IEEE-754 floating point, implemented by specifying IEEE-754 semantics in Coq, then using that to create a proof the compiler correctly preserves the semantics of IEEE-754 during the compilation process.

aseipp 10y ago

People doing theorem proving and formal methods know what complex numbers are, I can assure you. Mathematicians have plenty of statements about the properties of complex numbers, and many theorem provers have libraries that even formalize those statements and proofs in mechanized, automated ways that can be trusted. I'm not sure how "complex numbers are involved" is any more of a mystical problem than "finite-field arithmetic is involved" is a problem: it isn't. I think I get what you mean, though. No, you cannot prove "my drone is magical and awesome and will never crash land even if I tell it to, and it takes the best pictures of any drone". You cannot mathematically prove "My on-board sensor will always work and defy the laws of physics and never be inaccurate". You CAN mathematically prove "My drone control software never reaches an illegitimate state, that would cause the system to deadlock or hang due to a software error, making the drone crash in a possibly dangerous, uncontrolled way". You CAN prove "My software will respond within exactly N cycles, at most, to any external incoming sensor signal". That kind of guarantee is extremely valuable for such systems. It isn't easy (and requires deep, conjoined assumptions and proofs of both the hardware and software), but it's hardly impossible. And sure, there is only so much the model can prove to you, at some point it has to exist "in the real world". This isn't really a counter-point to the actual formal methods field, though. To couch it in a more concrete example: when people like Intel say "our CPUs don't catch on fire", they only mean it in a very specific sense. Sure, you can shove newspaper up next to your heatsink, and then when it catches on fire say "See! You were wrong!" But the reality is that their statement is sort of couched in the assumption that, well, you aren't going to do that. It's fairly reasonable to assume some limitations of your model. But this really has very little to do with being able to formalize general mathematics (like complex numbers or finite fields or N-dimensional spaces) using a theorem prover, or whatever.