Hacker News Reader

You cannot use unit tests for everything, since the number of unit tests required is basically infinity. Logically, unit tests can only prove an error exists and cannot show the program is correct. What they most likely did was mathematically showed that all possible edge cases (potentially inifinitely many) are all considered.

View on HN

I have never heard of verified compiler before. Not entirely sure if I understand everything from their docs either. But here are my thoughts.

Even though you cannot unit test everything. I would still prefer it, then to have another compiler pass to ensure C semantics are the same as the compiled code. Even though compiled code is the same as C. C code can be buggy from the start.

I don't understand the use of "mathematically proven" in this context as well. Proving that x86 add instruction or a set of x86 instruction has the same as the semantics of the C code, is just pure computer science problem, not mathematic?

Reply on news.ycombinator.com