Názor k článku HelenOS nikdy nebude dokončený, říká jeho autor Jakub Jermář od Sten - Přesně tak. Hlavní výhoda QNX není ani tak...

Přesně tak. Hlavní výhoda QNX není ani tak to, že je mikrokernel, tedy že se super udržuje, ale hlavně spolehlivost daná (zde zavrhovanou) schopností restartovat jednotlivé služby za běhu, což se ale nevyužívá jenom pro případ pádu, které budou reálné, i když budete mít svou část formálně verifikovanou (např. u jaderné elektrárny těžko může systém říct: balím to, dokud to neopravíte), ale taky pro aktualizace.

Mimochodem formální verifikace má jeden zásadní problém: samotná definice, podle které se ověřuje, může obsahovat chyby :-)