Igen , pont erről szól az egész, írták is a cikk végén , hogy ez egy végtelenül lecsupaszított kernel, aminek 100% helyességét még így sem lehetett egyszerű úgymond bizonyítani.
Egy komplett OS ennél sokkal , de sokkal , de még annál is sokkal összetettebb.. event handlerek, különböző space-ek, layerek kezelése és átjárhatósága közt kezelő közbenső rétegek... megjelenítő grafikai motorok, értelmezők, olyan szintű kesze-kuszasága, hogy egy földi halandó ennek egy al-al-al komponensének megértésébe is beleőszülne... ahol egy hiba nem sok de bőven elég ahhoz hogy boruljon az egész mint a kártyavár...
A pcforum.hu-n vagy a prog.hu-n volt egy cikk, hogy matematikailag helyességbizonyított operációs rendszert csináltak, bárki letöltheti, ingyenes, gondolom volt benne link is. VirtualBox-ban ki szerettem volna próbálni, de nem találom: a "helyességbizonyított", "helyességbizonyítás" kifejezésre kerestem rá mindkettőn. Valami ötlet? Köszi.