https://opennet.dev/openforum/vsluhforumID3/128671.html Компания Google объявила об открытии наработок, связанных с проектом KataOS, нацеленным на создание защищённой операционной системой для встраиваемого оборудования. Системные компоненты KataOS написаны на языке Rust и выполняются поверх микроядра seL4, для которого на системах RISC-V предоставлено математическое доказательство надёжности, свидетельствующее о полном соответствии кода спецификациям, заданным на формальном языке. Код проекта открыт под лицензией Apache 2.0...<br><br>Подробнее: https://www.opennet.ru/opennews/art.shtml?num=57920<br> https://opennet.dev/openforum/vsluhforumID3/128671.html#208 Sun, 23 Oct 2022 10:32:39 GMT &gt; Вот именно. На помойку. Любая проблема с памятью и всё, конец <br>&gt; железке.<br><br>ноотопы в помощь<br> https://opennet.dev/openforum/vsluhforumID3/128671.html#207 Thu, 20 Oct 2022 18:11:14 GMT &gt;&gt; Если что-то доказано, то оно доказано и это можно проверить механически<br><br>точно. проверить и проинтерпретировать. да?<br><br>ну математика оно такое как и любое знание<br>античные греки не знали вернее отметали идею нуля <br>ньютон прямо скажем читер<br>гаус с новой геометрией просто забоялся в отличии от лобачевского <br>кантор вроде числился современниками сумасшедшим<br>это я к тому что тут тоже не все так просто<br> https://opennet.dev/openforum/vsluhforumID3/128671.html#205 Thu, 20 Oct 2022 11:44:23 GMT Если что-то доказано, то оно доказано и это можно проверить механически, и никакие теоремы о неполноте этому не мешают. А соответствует-ли теорема спецификации, написанной на естественном языке - вопрос внематематический. И Гёдель, Пенроуз или Хофштадтер, как и любые другие люди, тут могут только тыкнуть пальцем в несоответствие спецификации и её формализации (если оно есть).<br> https://opennet.dev/openforum/vsluhforumID3/128671.html#204 Wed, 19 Oct 2022 10:56:47 GMT &gt; Если это про то, что формализация арифметики может быть противоречивой, то про <br>&gt; такое могут беспокоится только совсем выжившие из ума джедаи.<br><br>Скачай и прочитай &#171;Гёдель, Эшер, Бах: эта бесконечная гирлянда&#187;. А также &#171;Новый ум короля&#187;.<br> https://opennet.dev/openforum/vsluhforumID3/128671.html#203 Wed, 19 Oct 2022 10:55:12 GMT &gt; Если это про то, что формализация арифметики может быть противоречивой, то про <br>&gt; такое могут беспокоится только совсем выжившие из ума джедаи.<br><br>Так и не понял ты, юный падаван, суть математики.<br> https://opennet.dev/openforum/vsluhforumID3/128671.html#202 Wed, 19 Oct 2022 04:36:02 GMT Если ты пытался её запускать, то и неудивительно. С твоими-то когнитивными способностями.<br>А так вообще работает. И даже на реальном железе. Фотки на сайте можно посмотреть. <br> https://opennet.dev/openforum/vsluhforumID3/128671.html#201 Wed, 19 Oct 2022 04:30:09 GMT Сказал аноним в адрес корпорации с мультимиллиардным оборотом. :) <br> https://opennet.dev/openforum/vsluhforumID3/128671.html#200 Wed, 19 Oct 2022 04:26:22 GMT Вот именно. На помойку. Любая проблема с памятью и всё, конец железке. <br> https://opennet.dev/openforum/vsluhforumID3/128671.html#199 Wed, 19 Oct 2022 04:22:05 GMT Она ещё не готова просто, о взлёте говорить пока рано. Про другие фирмы есть что сказать? <br>