> А если серьезно, то пользователь может не знать, что вместо рекламируемых академиков код писали bunch of masturbating monkeys.В "нормальных" странах есть защита прав потребителя, даже если под соусом опенсурса и отказа от ответственности вам в код сунут зловредный код, то вы спокойно можете подать в уголовный суд, правда все это дело надо будет доказать.
> Есть хороший пример sel4 - где 6к строк кода верифицировали 11 человеко-лет.
А сколько человеко-лет заняло доказательство "последней теоремы Ферма"? Это нормально, ты думаешь над алгоритмом, строишь модель, доказываешь корректность, потом пишешь имплементацию по спеке на том или ином ЯК (языке кодирования) под ту или иную аппаратную архитектуру, остается только верифицировать итог. Проблема возникает когда мы себя обманываем используя в качестве ЯК не машинные КОП, а некоторый формальный ЯК уровнем выше, тот же Си. И возникает резонный вопрос, а мы компилятор вообще верифицировали? Как мы можем говорить о выше сказанном, если компилятор у нас не верифицирован, и тут верифицировать уже не только Си-шный код надо, но и выхлоп (сам компилятор тоже) компилятора (получается двойная работа). Справедливости ради, щас даже аппаратуру (ЦПУ, и проч. выч. технику) фактически начали выпускать без должной верификации, куда там за ПО говорить. Таков путь!
> Получилось невероятно надежно для СИшки, но очень-очень дорого.
Дорого для кого? Почем стоит ваша жизнь? Готовы доверить свою жизнь "кетайским" (не прошедшим выше описанные этапы) медицинским оборудованиям? Готовы стать пассажиром самолета, у которого из-за бага разгерметизировался салон? А сгореть заживо в какой-то тесле, где в ПО контроллера аккумулятора что-то пошло не так? Понятно, что рынок это спрос и предложение, если тот обреченный пользователь не думает об этом, и не желает "качественной жизни", то и так сойдет, пусть "падает и горит", он обречен по определению, а погромист - не обязан, все верно. Все беды людские от ума! Каждый достоин ровно того, чего заслуживает.
> Думаешь в опенБСД есть спецы такого уровня?
> Не тяпляпнуть код, а разбираться в алгоритмах и их верификации.
Хороших или плохих людей не бывает, бывают только хорошие и плохие поступки, они определяют человека. Если в опенБСД нет выше описанной практики (а ее во истину там нет), то с вероятностью 99.9999% и спецов возможно нет, но категорично говорить об этом нельзя, человек может знать и уметь, но не делать, потому-что и так за "дарма" (возможно, очередной АНБэшнйый "секурный" проект) делает, а потребителю плевать, что ему подадут на лопате.
> А потом в коньпиляторе поменяют СИшную UBшку (как произошлов C23) и код превратиться в ̶т̶ы̶к̶в̶у̶ не верифицированные буковки.
Все верно, выше я про это писал, не надо самообманываться, давайте признаем, что верифицированного ПО нет, так как нет верифицированной аппаратуры (ЦПУ и т.д.). Нельзя просто говорить о верификации опуская контекст аппаратный. Это связанные сущности. Даже если компилятор на выходе даст верифицированный результат не конкретной неверефицированной аппаратуры, а некоторой вычислительной модели (таже машина Тьюринга), то и это не показатель того, что на конкретной аппаратной архитектуре ПО будет считаться верифицированным.
> А где?
> Что ядро, что бсд оказались дырявыми.
> А к ним паравозом куча критических библиотек.
Не понял вопроса, что где? ОС - критическая система, от ее корректной работы зависит все прикладное ПО в том числе и критические библиотеки. Все взаимосвязано, выше указал, о связи еще с аппаратурой, если она не верифицирована, то что говорить о верификации ПО.
> писать корректный код)
> Я чуть сократил твои рассуждения.
Так Си, вся индустрия опенсурса (криптография и т.д.) на то и расчет, чтобы не было корректно. Любой безопасный (криптографически стойкий) алгоритм шифрования это угроза нац. безопасТности, поэтому АНБ всячески саботируют ее (яркий пример). Любая безопасная ОС или ЦПУ в свободном доступе (можно и на продажу, отсюда и всякие экспортные ограничения вытекают)- на руку "условному врагу", следовательно - угроза нац. безопасТности. Это все ведь очевидно. А потребитель - обречен по определению. Все о чем я говорю, о практике верификации, поверьте, там где нужно так и поступают, и не жалеют на это ни копейки бюджетных денег.
> Пресловутое AS IS когда пользователя ставят в положение "жричодали".
> И если на коммерцию есть хоть какие-то рычаги "исправьте баг, а то не увидите мои деньги", то на опенсорс - вообще никаких.
Чтобы такое сказать "а то не увидите мои деньги", надо иметь альтернативу на рынке, многие словца ради такое говорили "мелкомягким" - помогло? Не работает это, рынок - это кучка бандитов, порой сговариваются, порой симулируют конкуренцию, но всегда вертят вертят обывателя на сами знаете чем.
> Это можно решить законодательно.
Да, конечно, прописать ответственность за безответственность! :)
> Примерно как с продажей пирожков, шаурмы или оказания услуг (например медицинских).
Отравился и помер, жизнь не вернуть и что? Людей от голода больше гибнут чем от просроченных пирожков, вам ровно так и скажут, а самолеты самый безопасТный вид транспорта.
> Но опенсорсники первые выступили против.
> Удивительно, не правда ли.
Ну а кто не против, даром ведь и не навязчиво, вон булыжник из речки достал и бросил валяться на дороге, кто-то взял и брякнул им кому-то по кумполу, кто виноват? Тот кто брякнул, скажем "мы", но булыжник ведь не должен валять на дороге. Короче, такая примитивная аналогия.
Вариант для распечатки
(??), 17-Июл-26, 16:28
