Journal
Notes d’un ordinateur qui n’a rien d’autre à faire.
Comment NoWayOS est construit, et pourquoi. Chaque affirmation de ces pages s’accompagne de ses éléments de preuve, ou indique clairement qu’il ne s’agit encore que d’une conception.
React en entrée, Rust en sortie
Les designers gardent React. Les appareils reçoivent du Rust natif. Comment le Screen Compiler transforme les écrans en code à la compilation, pour qu’il n’y ait aucun navigateur à attaquer sur l’appareil.
Le secours qui n’était pas une copie
Apollo 11 emportait deux systèmes de guidage bâtis sur des principes différents, et a eu besoin des deux. Ariane 5 en emportait deux identiques, et une seule faute a arrêté les deux. Cette différence porte un nom, et NoWayOS est construit pour se trouver du bon côté.
Nous attaquons notre propre build à chaque modification
Un test de sécurité qui ne peut pas échouer ne prouve rien. Les tests de NoWayOS viennent donc avec des variantes faites pour échouer, et ses contrôles vivent là où une pull request ne peut pas les atteindre.
Ce qu’une preuve peut promettre
Un test essaie les cas auxquels quelqu’un a pensé. Une preuve les couvre tous. Ce que disent les preuves mathématiques de seL4, ce qu’elles supposent, et où se situe NoWayOS.
Pourquoi un appareil NoWayOS n’a pas de shell
La plupart des appareils dédiés sont des ordinateurs généralistes avec une tâche par-dessus et tout le reste encore en dessous. Nous avons pris l’autre route : construire chaque appareil avec seulement ce dont sa tâche a besoin, et laisser le reste de côté.