Hacker News Reader

Comment by etaioinshrdlu | Hacker News Reader

By the way, iOS devices also run a completely different OS on the secure enclave: https://sel4.systems/About/seL4-whitepaper.pdf

The SEL4 kernel is different because it has actually been "proved correct" and "proved secure" according to the authors.

View on HN

ObKnuth:

> Beware of bugs in the above code; I have only proved it correct, not tried it.

Layperson here: what does that mean?

It's a comment from a correspondence between Donald E. Knuth and Peter van Emde Boas (meant as a joke I think).

You can find it in this pdf at the end of the 7th page : https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf

Knuth mentions it in his FAQ (at the end) : https://www-cs-faculty.stanford.edu/~knuth/faq.html

I got that part. The part I don't understand is this: what does it mean for a program to be proven correct but still not work?

It means that the correctness properties that were formally proved are not necessarily what you would intuitively understand as "correct". E.g. you can formally prove that a buggy factorial(n) always outputs (n - 1)! by incorrectly defining what you want to prove. The function behaves according to what you proved, it's just not the expected behaviour.

More pointily: "correct" is not a formal property of a program, so you can't actually prove it in the first place. Rather you have proved some actual formal properties of the program (eg, always terminates, does not branch dependent on cryptographic secret data, etc[0]), which may, or may not, have any relevance to it's actual intended behviour.

0: Strictly speaking, even those are only English-language descriptions of formal properties, and you still need to worry about whether the formalization actually means what you think it means.

It's a joke. You'd expect that a proof of correctness to be the Holy Grail. Nothing could be wrong, since it's proved correct. And yet, after running it, you could still find a bug in it, because you may have made a mistake in your proof.

To the other comments here I have to add - proofs (in math, science, computer science, any subject area..) never reflect absolute reality, but rather just your view of reality or the parts of reality that you have chosen to model.

So the reality of your "proven" program will never 100% match the reality of it running on hardware or some other software context than you anticipated. Let's call this the Hacker's Postulate...

As for math specifically I think this is a very deep and interesting philosophical tangent to go down.

In addition to the sibling answers, one could have verified an algorithm mathematically, but made a typo in the code.

It’s a joke. https://en.m.wikipedia.org/wiki/Formal_verification

The Secure Enclave runs a custom L4 derivative, rather than seL4.

Reply on news.ycombinator.com