Понимание широкой команды, VLIW

как в этой ситуации поступит жит?

Щас бы сложные, неоднозначные и потенциально дырявые алгоритмы прошивать в железе. Даже если не в железе, а в ring0. Вердикт: не надо.

Можно же формально доказать, что эти оптимизации не меняют семантику кода. В качестве примера предлагаю nvidia с ее денвером, который ставят в автомотив, а там-то требования к надежности весьма и весьма.

Можно же формально доказать, что эти оптимизации не меняют семантику кода.

Кому доказать - сертифицирующему органу? Клиент-владелец может проверить прошивку? Формальное доказательство - это доказательство корректности модели, а не реального объекта.

В качестве примера предлагаю nvidia с ее денвером, который ставят в автомотив, а там-то требования к надежности весьма и весьма.

Какие такие требования у экспериментальной поделки частной компании не уважающей opensource?

экспериментальной поделки частной компании не уважающей opensource?

Я бы предложил пропустить этот лоровский булшит и иметь конструктивный диалог. Или не иметь его вовсе.

Кому доказать - сертифицирующему органу?

Я бы начал с доказательства разработчикам самой системы в первую очередь.

Формальное доказательство - это доказательство корректности модели, а не реального объекта.

Угу. А затем распространять формальщину дальше, пока не надоест, вплоть до формальнодоказанного компилятора: были бы ресурсы на это и желание.

Какие такие требования у экспериментальной поделки частной компании не уважающей opensource?

MISRA и что-то там еще? Я тут несведущ, увы, в процедуре сертификации по этим стандартам: не знаю, нужно ли им предоставлять исходники на ревью или же достаточно пройти набор тестов. В моей практике бывало всякое.

Я бы начал с доказательства разработчикам самой системы в первую очередь.

У формального доказателства есть проблема с тем, что это NP-полная задача. Так что, любая задача размера больше, чем хелло-ворлд на несколько тысяч строк - это уже практически нерешаемая задача, если заранее не знаешь эвристик, как решать такую задачу.

Я тут несведущ

Я тоже. То есть разговор про требования не имеет никаких (формальных) оснований.

(Пусть знающие люди расскажут как за какие гешефты сертифицируются реальные объекты, которые могут самовозгораться, путают рекламные знаки со знаками остановки и тд и тп)

Щас бы сложные, неоднозначные и потенциально дырявые алгоритмы прошивать в железе.

не понял что дырявого в том чтобы отправлять объекты на гпу, или в том, что камера захватывает то больше, то меньше объектов в зависимости от угла обзора, но ок.

ну можно конечно рассчитывать на то, что все алгоритмы линейные и их условная «сцена» всегда статическая. но мне кажется, что земля вращающаяся вокруг солнца, а луна вращающаяся вокруг земли готовы с этим поспорить, и наверное по большому счёту на линейность алгоритмов не стоит сильно рассчитывать.

хотя гравитация вполне может оказаться дырявой, там какие-то странные побочные эффекты на скоростях близких к скорости света. это не исключено.

У формального доказателства есть проблема с тем, что это NP-полная задача.

Это все правда, да. Тут, скорее, стоит говорить о том, что теоретическая возможность сделать полностью доказанную систему есть, но мало кто будет тратить на это необходимые ресурсы(особенно с точки зрения бизнеса). Поэтому доказываться, наверняка, будут какие-то совсем критичные куски.
Насчет верификации оптимизаций можно, например, посмотреть сюда: https://github.com/AliveToolkit/alive2
Боттомлайн предложу такой: да, полностью доказанная система это утопичный миф, но средства для того, чтобы повысить ее надежность до какой-то степени - есть.
Не стоит забывать, что в nvidia над этим проектом трудятся, пожалуй, одни из самых лучших специалистов в области бинарной трансляции, поэтому они куда лучше представляют все сопутствующие проблемы и их возможные решения.