Исходный код «самой надёжной в мире ОС» seL4 microkernel будет открыт через месяц

> Кроме того, двоичный код, выполняемый на оборудовании правильно транслируется в код C, а это значит, что компилятору не стоит доверять и функциональная точность проверяется для бинарного кода.

Нашёл в оригинале исходную фразу:

seL4 has full ‘functional correctness proof’, so the implementation (written in C) adheres to its specification. Also, the binary code that executes on the hardware is a correct translation of the C code, meaning that the compiler does not have to be trusted and extends the functional correctness property to the binary.

Могу предложить более адекватный перевод, как минимум он точнее:

sel4 имеет полное «доказательство функциональной корректности», то есть доказательство того, что реализация (написанная на C) точно соответствует спецификациям. Кроме того, двоичный код, выполняемый на оборудовании является точной трансляцией кода на C, что гарантируется тем, что разработчики не доверяют компилятору и выполняют проверку функциональной точности ещё и для бинарного кода.

Помимо коррекции общего смысла в нюансах кто куда транслируется, в этом переводе я перевожу слово «proof» словом «доказательство», что довольно-таки критично, поскольку речь, очевидно, идёт именно о том, чтобы строго доказать корректность кода. Задача, вообще, не из лёгких, но когда очень хочется, и когда строк кода всего 8700, видимо возможно.