Здравствуйте, alpha21264, Вы писали:

A>Мне совершенно непонятно, почему Винду нужно неперывно обновлять.
A>Они что, с самого начала не могли правильно сделать?

Если речь об обновлениях безопасности, то тут все достаточно просто. Используемые языки программирования (C/C++) не позволяют создавать код с хорошим уровнем надежности. Как следствие, любая версия ОС (в том числе и с последними патчами), написанная на этих языках, неизбежно содержит массу дыр, больших и маленьких. Микрософт постоянно затыкает одни дыры и создает другие. Вот такая "безопасность".

Остальные распространенные операционные системы подвержены ровно тем же проблемам. Верификация кода с помощью существующих средств требует очень много времени и очень высокой квалификации исполнителей, поэтому в настоящее время особенно не применяется. Существует формально верифицированное микроядро L4.Verified, на примере которого видно, чего стоит верификация:

https://ts.data61.csiro.au/projects/TS/l4.verified/numbers.pml

How big is seL4?

8,700 lines of C code plus 600 lines of ARM assembly code.

How big is the proof?

All together 200,000 lines of Isabelle proof script. Manually written, machine checked. Roughly 3,500 A4 pages if printed out (a stack about half a meter high).

How much work was it?

In total, design, documentation, implementation and verification of the seL4 kernel come to about 25 person years. This includes a lot of new research, new tools, and new libraries. If we were to do it again, we think it would be less than 10 person years.

Теперь если представить, что вместо 7000 строк кода у нас есть 50 миллионов строк, которые постоянно изменяются...


Вывод из всего этого один: необходимы более безопасные языки программирования.