Azon gondolkodtam, hogy ahogy volt hír a svájci mikrokernelről, amely kódjának hibamentességét 2 éven át bizonyították - vajon nem érné meg az iparnak létrehozni olyan szoftveres építőköveket, melyek nem változnak gyorsan a trendekkel, nagy mértékben használtak, előre is lehetne tervezni velük - és megpróbálnák bizonyítani a kód helyességét?
Lehetetlen feladat? Vajon lehetetlen lenne meghatározni és kiválasztani ezen építőköveket? Vagy egyáltalán előre tervezni vele? Nem lehetne külön lib-eket kiadni egyetemeknek a bizonyításhoz? Muszáj minden szoftvert folyamatosan görgetni és új feature-ökkel ellátni? Az építőköveknél nem kellene hogy legyen ilyen motiváció szerintem. A for profit cégeknél értem, de talán nagy részét le lehetne fedni így az iparban használt szoftverek hibáinak.