Hacker News Reader

Comment by jojo2000 | Hacker News Reader

jojo2000

In the automotive and aerospace world, of course tests in the real world cannot cover all cases (cost, time make it impossible).

Even most (not all, but almost none for meaningful applications) computer program cannot be proved to come to an halt [0], so complete testing is impossible by essence. We can only use more restrictive rules for programming but cannot formally guarantee anything.

As those systems are tied to the physical world, a whole lot of complexity is added by uncontrolled parameters.

Yet we love testing things. So a lot of techniques exist, such as SIL [1] and HIL [2].

So you could imagine using a real dashboard hooked up to a plane simulator. Which would enable testing the device in a wide array of conditions.

[0] https://en.wikipedia.org/wiki/Halting_problem [1] https://www.quora.com/What-is-Software-in-the-Loop-SIL [2] https://en.wikipedia.org/wiki/Hardware-in-the-loop_simulatio...

View on HN

> Even most (not all, but almost none for meaningful applications) computer program cannot be proved to come to an halt

That is not true. If you can demonstrate that every loop or recursion is bounded, then the program must halt as a necessity. Loops of the form for (i = 0; i < N; i++) are trivially bounded, unless you're resetting i in the loop. If you have containers that are not being modified in the loop, the finiteness of your data structures is usually sufficient to form the lemma that the loop will terminate.

Recursive datastructures (such as cyclic graphs) are much more challenging to prove, and most challenging are fixed point algorithms (do { } while (changed);), as will be noted by them frequently being the causes of actual infinite loops in my experience. But if you had mandatory annotations to declare lemmas for termination, it is doable. With that feature, a programming environment that forbade you from writing code that couldn't be proven to terminate is probably sufficiently feasible to allow you to write large, complex applications.

My POV here was very cautious, as I didn't exclude programs which can be proved. The problem is that even if control flow is "provable", a lot of algorithms use number computations and is much harder to deal with from a formal POV :

"In cooperation with the University of Iowa and Rockwell Collins, this research focuses on the verification of safety properties on Lustre pro-grams. SAT or SMT, based verification approaches such as k-induction give good results on programs with a mostly discrete state space (boolean, bounded integers). However, when numerical computations are involved (real/float computations) the formalization of the property to be proved often needs to be strengthened using auxiliary lemmas to make it inductive with respect to the system’s transition relation. When attempted manually the discovery of such lemmas is time consuming and hinders the efficiency and scalability of formal verification. Automating lemma discovery hence appears crucial to allowing end-users to apply formal verification on industrial cases."

Taken from [0]

The seminars I attended to, from the creators of coq (a formal verification language), didn't disagree with this point of view. Of course, formal verification is not the only thing we can do [0].

In any case, what you propose seem interesting, if the halting problem was the only problem to solve to have a formally proven system.

[0] http://www.aerospacelab-journal.org/sites/www.aerospacelab-j...

Reply on news.ycombinator.com