Comment by mkleczek | Hacker News Reader

Comment by mkleczek | Hacker News Reader

Parent Full thread

> I don't think your reply is particularly effective when you are replying to a comment that exhibits a formally verified microkernel.

I would say that one small piece of software (Sel4 is only 9,400 SLOC!) always cited as an example is actually a very small set of programs that can be formally verified. I haven't heard of a formally verified web browser...

> Many useful algorithms can be proven to terminate.

Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.

> But it is clear for example that if, say a program is recognized by inspection as the concatenation (splicing the final states and initial states together) of two programs that terminate, then this program terminates

But it does not tell us anything about real programs? We don't compose software by concatenating their state machines.

> Even the link you provide gives optimism and claims that

This is a call for empiricism (aka testing) and ad-hoc heuristics exactly because the problem is not solvable in general using formal methods.

I misunderstood the goalposts because you had seemed to be talking about theoretical CS notions like complexity and computability (we were talking about the halting problem), and now you are talking about proving properties motivated outside TCS.

> Proving that a program terminates is not that much interesting. Lack of security vulnerabilities would be much better.

My bad, I dare make the stronger claim that most algorithms that you see in an undergrad algorithms textbook are useful and mathematically known to be correct.

> But it does not tell us anything about real programs?

I agree that most software today are extremely complicated. Most software today don't even have a proper target specification all in one place, which is kind of a prerequisite for being proven to adhere to a specification. Furthermore, most software today is so complex that attempts at a rigorous specification is likely to have bugs at the level of stating the property itself. Not to mention completely missing properties that one is unaware of that are relevant to attacks that one is unaware of.

But core parts of real software is composed of those undergrad algorithms that are proven to be correct. You can create useful libraries of useful algorithms that have guarantees, and small programs that have guarantees. For this reason I disagree that the class of useful programs is as small as you think.

> We don't compose software by concatenating their state machines.

Structured programming without loops can be modeled as concatenation of turing machines (branching composes different machines to the accept and reject states); and it is trivial that it terminates once the component machines terminate.

When you introduce a loop that is when you need to identify a nontrivial property that guarantees that the loop terminates, and this is done work for many useful algorithms.

Reply on news.ycombinator.com