Hacker News Reader

> tools to come with solutions that allow to proof that code is correct

I may be misunderstanding, but isn't part of the problem that these tools are themselves written in code and therefore subject to bugs?

View on HN

This is addressed by the de Bruijn Criterion. The essential idea is that a small number of "trusted" rules should be enough to satisfy even the largest proofs. You have to keep the number of rules small enough that they can be reviewed and understood by humans so that you can trust the proofs verified by the kernel.

That probably helps to reduce the occurrence of issues, but I feel you are still ultimately relying on the correctness of proof assistants like Coq. And I am sure that bugs are occasionally found in Coq!

Indeed it does happen and it's unavoidable. You have to pick your axioms from somewhere and sometimes we pick the wrong ones or we find errors in our definitions. There's no "complete" or "perfect" system.

There are verified compilers such as the compcert compiler and also ways to verify that a given binary does in fact correctly implement an specification

Reply on news.ycombinator.com