Hacker News Reader

Comment by markusde | Hacker News Reader

This is a good but also misunderstood point. It is true that you can't automatically do this in general. However, expressive enough type systems can contain human-written, machine-checked proofs of (models of) these properties. I think the jury's still out on whether or not humans or machines are better at coming up with proofs, but computers are decisively a lot better at checking them than we are.

The way I see it formal methods not a holy grail where we don't have to think about the code we're writing anymore, but it is a very strong next step from "I wrote this code and here's why I think it's right" to "I wrote this code and here's a machine-checked proof that it's right". Effective automation can make that step easier to take in a lot of real-world cases.

View on HN

It’s not about automatically doing it — it’s about for many cases there can’t exist a proof. And it is not even some theoretically interesting but never happening case, but quite trivial programs will quickly come to this state. Sure you can restrict some things, like boundless loops, but the “beauty” of complexity and the limit of our very mathematics won’t disappear, unless you go to too trivial systems which are useless. See my other comment for an example.

I remember there being an analogy between Gödel’s incompleteness theorem as well, which is also only true to “expressive enough” systems (where you can basically do integer math) — but I may be talking completely out of my arse at this point.

I get your point, and I agree with it too. My comment is (trying to) say that in those cases we don't know that humans are any better!

Your other comment has some problems, but a better example is

fn collatz(mut n: bigint, mut v: Vec<...>) {

  loop {

     n = { if n%2==0 then n/2 else 3\*n+1 };

     v.push(...);

  }

}

As far as we know, we can't bound the memory usage of this program: and if any FM can do it as well then there's a million bucks on the table. But so far no human can do it either! And if your program relies on this program using bounded memory, from an engineering perspective you're kind of SOL no matter what.

On the other hand, if you're writing programs which humans are pretty sure they know why the properties they want hold (as we usually try to do, anyways), then translating this into a machine-checked proof can give you a lot more faith that the property actually holds and possibly even find flaws in your reasoning/implementation if there are any!

Yes I agree with you on every point (though didn’t want to use the “heavy gunner” Collatz as an example :D). I’m not against dependent types, and I eagerly await what future might they bring. But at the same time I think the best solution will be to “fight on multiple fronts”, and improve our type and test systems. There are very interesting ways to systematically test every kind of input (greatly reducing the input space) that has a distinct code path (and it can find a minimal reproducible error case!).

Well one thing programmers do often due to the complexity of formal proof is random property testing instead. Mathematicians do so too, which is why the Collatz conjecture is a conjecture in the first place. There is an alternative to Software Foundations that uses randomized property checking. It would be interesting to have a hybrid system where we independently give specifications and then decide whether we wanted to formally prove them or just do tests instead.

Reply on news.ycombinator.com