Исходное сообщение
"Google открыл код защищённой операционной системы KataOS" Отправлено red75prime, 20-Окт-22 14:44
Если что-то доказано, то оно доказано и это можно проверить механически, и никакие теоремы о неполноте этому не мешают. А соответствует-ли теорема спецификации, написанной на естественном языке - вопрос внематематический. И Гёдель, Пенроуз или Хофштадтер, как и любые другие люди, тут могут только тыкнуть пальцем в несоответствие спецификации и её формализации (если оно есть).