Исходное сообщение
"Увидел свет Debian GNU/Hurd 2017" Отправлено Аноним84701, 19-Июн-17 15:16
>> bash, wget > ЧТО, вы в своем уме вообще-то? Всё спокойно влезает, микроядра тоже верифицируют > (L4 правда, а не Mach). Вы случайно не интересовались всякими "второстепенными" деталями? https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf > seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. А теперь смотрим человеко-часы (точнее, годы): > The overall size of the proof, including framework, libraries, and generated proofs (not shown in the table) is 200,000 lines of Isabelle script. >  The abstract spec took about 4 person months (pm) to develop. About 2 person years (py) went into the Haskell prototype (over all project phases), including design, documentation, coding, and testing. > for a total cost of 2.2 py including the Haskell effort. А ведь в wget более 40, а в баше вообще под две сотни тысяч cтрок кода. > Сейчас самая продвинутая верификация на системах > теории типов, получается весьма компактно и вычислить можно. Это все круто, но вы что-то серьезнее приветов миру верифицировать пытались?