На самом деле, UB оказалось не нужно

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

Чувак, ну вот свежая новость с Opennet недельной давности. На ЛОРе тоже вроде было.

https://www.opennet.ru/opennews/art.shtml?num=63104

Ты сам-то как думаешь, что такое «математическое доказательство надёжности»? Математики собрались под водовку и сказали: «слово пац^Wматематика, это надёжно!», так что ли?

Или может…

Код HACL* написан на подмножестве функционального языка F*, предлагающем систему зависимых типов и уточнений, позволяющих задавать точные спецификации (математическую модель) и гарантировать отсутствие ошибок в реализации при помощи SMT-формул и вспомогательных инструментов доказательства. Эталонный код на F* транслируется в код на языке Си при помощи компилятора KaRaMeL и доступен для интеграции с другими проектами.

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

Однако, несмотря на это, надо же было найти настолько неудачный пример. В первых же комментах к новости по ссылке объясняют почему это всё шум на ровном месте. И я с их объяснениями согласен. И добавлю ещё: уверен, эти «доказывальщики» про актуальные проблемы типа атак по таймингам проца вообще не в курсе, и доказывали только то что в коде этой библиотеки действительно закодена заявленная математика (надёжность которой они тоже разумеется доказывать и не пытались) - то есть занимались чуть менее чем полностью бесполезной активностью. И повторюсь, основные два применения этой штуке: 1) производить впечатление на нубов «мы не просто кодеры, мы ещё и математически доказали что мы правы, 2) удовлетворять всякие гос надзоры (впрочем это пересекается с пунктом 1).

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

Разворачиваю мысль: верифицировать алгоритм обычно обозначает переписать его на другом, сухом и строгом, математическом языке. Что для такой сложной программы как компилятор может быть просто неподъёмной задачей. Но стремиться всеравно стоит. Чем больше формальных доказательств имеется и чем более сложны верифицированные задачи, тем лучше. Так как можно не начинать с нуля, а пытаться свести некую новую к уже имеющимся и если достаточно аккуратно это сделать, то смело считать её решение тоже верным.

И добавлю ещё: уверен, эти «доказывальщики» про актуальные проблемы типа атак по таймингам проца вообще не в курсе

Ещё как в курсе. Зачем вы мешаете всё в одну кучу и теорию и практику.

Разворачиваю мысль: верифицировать алгоритм обычно обозначает переписать его на другом, сухом и строгом, математическом языке. Что для такой сложной программы как компилятор может быть просто неподъёмной задачей.

У тебя просто будут баги в ходе конвертации ТЗ, написанного бытовым языком, в этот самый «сухой и строгий» язык. То есть алгоритм на «сухом и строгом языке» в бинарник у тебя превратится корректно и ты будешь уверен, что бинарник соответствует тому что ему подали на вход, но вот сам по себе алгоритм будет не тот что хотел заказчик. Собственно, при обычном программировании на Си происходит ровно то же самое: компилятор полностью корректно превращает твою писанину в бинарник, проблема в том что писанина расходится с желаниями (в т.ч. теми которые вообще нигде не сформулированы иногда). Изначально строго сформулированная задача есть только у уже упомянутых числодробилок. Как вы не поймёте, что проблема вообще не в том месте где вы её представляете.

Ещё как в курсе. Зачем вы мешаете всё в одну кучу и теорию и практику.

Вот вот, есть бесполезные теоретики-графоманы и есть полезная практика. Я как раз намекал что стоит смотреть на второе.

У тебя просто будут баги в ходе конвертации ТЗ, написанного бытовым языком, в этот самый «сухой и строгий» язык.

Совершенно верно.

Вот вот, есть бесполезные теоретики-графоманы и есть полезная практика. Я как раз намекал что стоит смотреть на второе.

Возможно и стоит, но точно не исключает. Не совсем понимаю где тут несогласие.

«Программа корректно обрабатывает любой ввод, который мы смогли придумать и выдерживает любой фаззинг, который мы смогли провести» – отличное достижение.

И в то же время «Программа верна вообще для любого возможного ввода и при этом имеет такую-то временную и пространственную сложность» – ещё более ценное достижение.

Программа корректно обрабатывает любой ввод, который мы смогли придумать

Программа верна вообще для любого возможного ввода

«Программа не вылетела с сегфолтом», «программа не вывела мусор на выходе» и «программа отработала именно так, как хотел заказчик» - это всё разные вещи, не надо их кидать в одну кучу.

Ладно, я согласен что проверка на отсутствие сегфолтов и прочей порчи данных полезна, но не надо её выставлять за «мы доказали что программа верна». Верна - это когда заказчик скажет «да, я именно это хотел» (на каждую итерацию фаззинга итд), и никакие автоматические инструменты это принципиально не могут обеспечить. За исключением, повторюсь, задач, которые изначально сформулированы математиками.

проверка на отсутствие сегфолтов и прочей порчи данных полезна, но не надо её выставлять за «мы доказали что программа верна»

Я и не выставлял, это очень разные задачи, с огромным различием по сложности (трудоёмкости, выполнимости).

Верна - это когда заказчик скажет «да, я именно это хотел»

Ок, это одно из возможных определений термина «программа верна».🙃

Во-первых, ты опять (первый раз это сделал не ты а@opcode) подсунул вместо прикладной программы математическую числодробилку, про которую я и не отрицал что там есть что доказывать.

Окей, вот тебе ядро ОС с доказательством корректности: https://sel4.systems/

Достаточно прикладная программа?

Там «доказано», что сисколл open(O_CREAT|O_NOFOLLOW|O_TRUNC) (или его аналог если оно не posix) действительно открывает файл, создаёт его если его нет, обнуляет размер если есть, не следует симинку в последней части пути но следует в остальных, правиьно проверяет uid:gid и прочие права доступа и правиьно репртит i/o ошики в приложение?

В seL4 нет аналога такому сисколу, это микроядро, т.е. по сути брокер сообщений между процессами.

То есть они доказывали, что сообщение, отправленное одним процессом, придёт в другой, который его получатель? Определённо, крайне полезная деятельность. Хотя мне сложно представить, что именно там является предметом доказательства.

А hateyoufeel, получается, наврал, это никакое не «ядро ОС».

А hateyoufeel, получается, наврал, это никакое не «ядро ОС».

А что же это тогда, блд? Чувак, не тупи.

Тебе нагнали, это не просто брокер сообщений. Это абстракция от железа и реализация модели разделения времени CPU и памяти в первую очередь. То есть, ядро ОС. Передача сообщений – часть интерфейса для процессов, во многом превосходящая сисколлы.

И что именно там доказали и зачем?

С точки зрения сисколлов - брокер. Так-то понятно, что там много чего ещё есть.

что именно там доказали

Процитирую их сайт для Ъ:

Functional correctness: the C code of all verified configurations of seL4 behaves precisely as specified in the seL4 specification and nothing more. This is the strongest assurance that the code will not have any unspecified behaviour.

Binary correctness: in the configurations that support this property, the binary machine code running on the processor correctly implements the behaviour of the C code assumed in the functional correctness proof. By extension, this means the binary code implements precisely the behaviour of the specification, and nothing more.

Security: in the configurations that support this property, the specification, and by extension the kernel code, prevents an application running on top of seL4 from modifying data without authorisation (integrity), from interfering with resource access of other applications (availability), and from learning information from other applications without explicit authorisation (confidentiality). Together these security properties enforce the isolation of components running on top of the kernel, allowing critical components to securely run alongside untrusted software.

зачем

Зачем нужно ядро, которое 100% гарантированно не вылетит с паникой? Чувак, я даже не знаю.

Кстати, они ещё и компилятор Си породили, который гарантированно выдаёт бинарник с поведением, описанным в исходном коде.

С точки зрения сисколлов - брокер. Так-то понятно, что там много чего ещё есть.

Что такое «с точки зрения сисколлов»? Если ты имеешь ввиду, что там по сути один сисколл – передать сообщение, то и насрать 100 раз. Это просто деталь API.

as specified in the seL4 specification

Возвращаемся.

1) На каком языке написана спецификация?

2а) Если она написана на обычном английском - их доказательство включает в себя его строгий интерпретатор?

2б) Если она написана на каком-то формальном языке - чем это лучше ситуации, когда мы код на Си объявим спецификацией, и он автоматически будет сам себе соответствовать?

Зачем нужно ядро, которое 100% гарантированно не вылетит с паникой? Чувак, я даже не знаю.

Нет там таких гарантий, не выдумывай. Битое железо, битовые флуктуации в небитом железе и уязвимое железо никто не отменял. Что касается чисто алгоритма, то просто ручная проверка кода без всего этого теоретического задротства даст тот же результат. Разумеется, к огромным ядрам современных ОС она непосильна, но они и не написали такое ядро.

Нет там таких гарантий, не выдумывай.

Есть, на код.

Битое железо, битовые флуктуации

ECC.

уязвимое железо

Проблемы другого порядка.

просто ручная проверка кода без всего этого теоретического задротства даст тот же результат

Сразу видно кукаретика. Внесли новую фичу – четыре месяца регрессионного тестирования и ФОТ в десятки миллионов в год на QA отдел.

Это здорово.

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

Комменты в теме еще не было времени прочитать, но там же как обычно треш и угар, да? =)

Так в том и дело, что проблемы бывают в разных местах, не только в коде. ECC не от всего помогает, и его не везде возможно впихнуть. Про миррор-мультипроц бы лучше вспомнил.

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

Внесли новую фичу – четыре месяца регрессионного тестирования

Так там «микроядро», что ты туда вносить собрался? Они как раз приняли все меры к тому, чтобы все фичи по возможности были во внешних модулях (за которые они не отвечают), разумеется при таком подходе контроль качества кода делать проще. Но не надо всё это приписывать исключительно теоретикам-доказателям.

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

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

Так в том и дело, что проблемы бывают в разных местах, не только в коде. ECC не от всего помогает, и его не везде возможно впихнуть.

Это отдельная история, опять же.

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

Я не понимаю что ты пытаешься доказать. Что формальная верификация кода не нужна потому что ошибки могут быть где-то ещё? Но это тупое утверждение, зачем ты его делаешь? Очевидно, что чем меньше ошибок, тем лучше.

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

Все так. Система разбивается на отдельные модули и ошибки старательно устраняются в каждом. Часть резервируется. Таким образом достигается надежность систем. Если горестно вскидывать руки что процессор может сгореть, а значит не надо код тестировать, то мы так далеко не уедем.

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

Это ты сам увидел, тут никто такого не говорил.

Сходи уже по ссылке, которую тебе дали, почитай. https://sel4.systems/Verification/proofs.html

На каком языке написана спецификация?

Спецификация написана с использованием (интерактивного) языка проверки теорем Isabelle/HOL. Этот язык покруче «кацелярита»

их доказательство включает в себя его строгий интерпретатор?

Да, этот язык (ядро языка Isabelle/HOL) основан на математических теориях. Например, https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

чем это лучше ситуации, когда мы код на Си объявим спецификацией, и он автоматически будет сам себе соответствовать?

Язык программирования Си не основан на мат.теориях. С соответствующими (не)математическими (не)гарантиями. Все гарантии даются только «по понятиям», хорошо, хотя бы задокументированным в стандарте.

математических теориях

Полтора землекопа

Полтора землекопа

Согласен, «по понятиям» жить проще.

От забора до завершающего нуля.

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

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

2б) Если она написана на каком-то формальном языке - чем это лучше ситуации, когда мы код на Си объявим спецификацией, и он автоматически будет сам себе соответствовать?

Потому что у языка Си нет однозначной строгой спецификации. Смотри в заголовок этого треда.

Нет там таких гарантий, не выдумывай

Есть.

Что касается чисто алгоритма, то просто ручная проверка кода без всего этого теоретического задротства даст тот же результат.

Что такое «ручная проверка»?

Это значит внимательно смотришь на код, мысленно трассируешь все варианты его исполнения и проверяешь что там нужный результат. Этим занимается, по-моему, очень много кто.

Ну, то есть, гарантией тут выступает слово пацана.

Гарантией что алгоритм на том самом формальном языке правильный (соответствует желаниям пользователя) - тоже. Ничего другого принципиально не может быть, до тех пор пока ты не сделаешь формальный строгий интерпретатор естественного языка. Который, разумеется, тоже невозможен потому как естественный язык сам по себе не строгий.

Гарантией что алгоритм на том самом формальном языке правильный (соответствует желаниям пользователя) - тоже.

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

В любом случае, у seL4 вполне доказанно багов на строчку кода сильно-сильно меньше чем у лялекса. Наверное, это просто совпадение, и мат.доказательство корректности тут не при делах.

Нет. Там гарантий гораздо больше.

Гарантии либо есть, либо нет. Повторю в третий раз, в итоге всё всё равно упирается в переход от бытового описания функционала к какому-то формальному языку, в отношении которого строгие доказательства невозможны. Все дальнейшие преобразования по сути просто разные виды компиляторов. И я считаю, что компилятор Си вполне хорош в этой роли, несмотря на то что он не удовлетворяет каким-то твоим теоретическим критериям.

В любом случае, у seL4 вполне доказанно багов на строчку кода сильно-сильно меньше чем у лялекса. Наверное, это просто совпадение, и мат.доказательство корректности тут не при делах.

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

И я считаю, что компилятор Си вполне хорош в этой роли, несмотря на то что он не удовлетворяет каким-то твоим теоретическим критериям.

Ты считаешь неправильно. Считай лучше.

Гарантии либо есть, либо нет.

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

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

Повторяй хоть 10 раз. Доказательства по ссылке, можешь скачать и ознакомиться.

И я считаю, что компилятор Си вполне хорош в этой роли, несмотря на то что он не удовлетворяет каким-то твоим теоретическим критериям.

А не ты ли выше писал:

Да, [разработчики компилятора] не правы.

То что -O2 сломан я в курсе

Ты оперделись уже: либо у тебя компилятор Си вполне хорош, либо компиляторы Си сломаны и делают говнокод.

Кстати, для seL4 был написан специальный компилятор Си – Compcert, для которого тоже доказана корректность. Написан, к слову, не на Си.

То, что они его проверяли с помощью своей математики - уже вторично, и я не знаю насколько повлияло на итог.

Нет, это первичное свойство этого микроядра. Собственно, ради него весь проект и был затеян.

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

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

мы всё посчитали и доказали, что тут всё норм

Они это не доказывали. Они доказали что код соответствует каким-то формулам. А вот то, что эти самые формулы соответствуют сформулированным на обычном языке требованиям, доказательств нет и быть не может. Я точно так же могу заявить, что мой код на Си доказанно соответствует моему коду на Си (по причине полного совпадения).

Ты оперделись уже: либо у тебя компилятор Си вполне хорош, либо компиляторы Си сломаны и делают говнокод.

Уточню: речь была про компилятор без сломанных опций. Мне казалось это очевидно. Если сложно - просто ставь везде -O0.

И там, конечно, не просто «посмотреть глазами и в уме прогнать», а очень долгое и тщательное тестирование.

Одно другого не заменяет.

сформулированным на обычном языке требованиям

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

Формулы понимают не только человеки, но и нечеловечеки - инструменты, которые не подвержены человеческим настроениям. Инструменты могут одинаковые (логически корректные) формулы интерпретировать одинаково.

Это свойство инструментов - повторяемость результата - самое ценное.

Если инструмент в виде компилятора Си по разному интерпретирует-исполняет инструкцию (с UB) - это проблема для человека. Либо инструмент нерабочий, либо инструкции неправильные.

Пиши правильные инструкции (формулы) для исправного инструмента.

Они доказали что код соответствует каким-то формулам. А вот то, что эти самые формулы соответствуют сформулированным на обычном языке требованиям, доказательств нет и быть не может.

А они не нужны. Формулы здесь первичны.

Я точно так же могу заявить, что мой код на Си доказанно соответствует моему коду на Си (по причине полного совпадения).

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

Уточню: речь была про компилятор без сломанных опций. Мне казалось это очевидно. Если сложно - просто ставь везде -O0.

Кто тебе сказал, что выхлоп компилятора с -O0 не будет сломан? Я вот этого не знаю про gcc или clang. Но я точно знаю, что в GCC были баги, из-за которых даже при сборке с -O0 получалась херня.

И там, конечно, не просто «посмотреть глазами и в уме прогнать», а очень долгое и тщательное тестирование.

Одно другого не заменяет.

«Прогнать в уме» не является доказательством вообще ничего, поэтому серьёзно рассуждать об этом – достаточно глупая затея. Это же подтверждают все срачи про UB, которыми я тут себя развлекаю: одни сишники говорят, что компилятор сломан, другие – что я не умею в Си, третьи – что стандарт говно и язычок надо на помойку. Кому из них тут верить-то? Нипаааняяяятнаааааааа!

Но вообще, мне нравится, как ты с помощью компьютера, изобретённого математиками, разработанного математиками и во многом верифицированного этой самой математикой (хардварь сейчас верифицируется примерно как seL4 выше, потому что баг в хардвари – это очень и очень дорого!) пишешь, что эта вся математика не нужна и вот сишники-то точно знают как делать безглючный софт.

Это переделанное условие не равноценно исходному,

Оно равноценно при заданных стандартном условиях: переполнение числа со знаком – UB.

Если бы в стандарте было бы другое написано, то компилятор бы не мог выполнить эту замену в данном случае. А так – может.

но багоделам, которые писали компилятор, плевать.

При чем тут «багоделы, которые писали компилятор», если поведение программы описано в стандарте?

Возьмём такой пример на Си-подобном псевдоязыке:

void f(integer x)
{
    integer a = 1;
    while (a <= 10) {
        print(a * x);
        a++;
    }
}

От Си наш воображаемый язык отличается тем, что integer здесь это целые числа в математическом смысле. (Предположим, что там под капотом используется куча, и пока ОЗУ хватает, мы можем числа любой длины вычислять.)

Перепишем теперь этот код, чтобы избавиться от 10 умножений и заменить на более эффективные сложения:

void f(integer x)
{
    integer a = x;
    integer limit = x * 10;
    while (a <= limit) {
        print(a);
        a += x;
    }
}

Результат исполнения программы будет идентичен. Эти алгоритмы эквивалентны.

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

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

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

Т.е. если можешь оптимизировать - оптимизируй. Не можешь - не оптимизируй, пускай программист сам переписывает алгоритм на более оптимальный. А портить язык в угоду говнокоду - осуждаю такой подход.

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

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

Лол нет. Всё тормозит по куче причин, и сложность чтения кода тут не причём. Навскидку:

1. использование вагонов жирных библиотек с готовым кодом, в каждую из которой напихано до жопы всего;
2. кучи непрямых вызовов и прочих виртуальных функций, из-за которых полностью отсутствует локальность и кэш оказывается постоянно просран;
3. повсеместные IPC/RPC. Любая софтина на электроне – несколько процессов, которые постоянно общаются между собой;
4. как следствие предыдущего, постоянная синхронизация. Мютексы – это меееедлеееееенннооооооооооооооооооооооооооооо…
5. интерпретируемые однопоточные язычки с JIT типа пердона и js. Ну ты понял;
6. альтернатива предыдущему – компиляторы, генеращие чудовищно раздутый код. Что C++, что Rust, что GHC, все этим страдают сейчас, выдавая бинарники в десятки метров размером. Что ни говори, но когда твоя прога не влезает в кэш проца, на скорости это положительно не сказывается.

А код современного говнософта читать куда сложнее чем даже сишных копролитов. Я серьёзно. Самый простой и читаемый код встречается в основном в хобби-проектах типа OpenBSD.

Но ты же согласился со мной по всем пунктам практически. Всё, что ты описал - делается для того, чтобы человеку было проще читать и писать код, а не машине. Человеку проще подключить библиотеку и заюзать 0.001% от её функционала. Машине лучше, когда человек возьмёт и сам реализует этот функционал, вместо подключения библиотеки. То же по всем остальным пунктам, включая OpenBSD. Ну насчёт генерации раздутого кода я хз, по-моему компиляторы С страшно умные и если они и генерируют раздутый код, значит так надо. Мой код в килобайты вмещается без каких-то особых усилий, не замечал я раздувания на ровном месте, я, конечно, с -Os компилирую, но с -O2 принципиальной разницы нет.

Оно равноценно при заданных стандартном условиях: переполнение числа со знаком – UB.

Оно не равноценно потому что систематически даёт разный результат работы программы. Что там награфоманили какие-то теоретики тут совершенно не важно, есть «экспериментальный» факт, который приоритетнее всего остального.

Но ты же согласился со мной по всем пунктам практически. Всё, что ты описал - делается для того, чтобы человеку было проще читать и писать код, а не машине.

Нет. Читать этот код почти невозможно. Писать его тоже может быть долго и сложно. Во многом это проблема отсутствия культуры разработки, крайне раздутых требований и стремления использовать сложные штуки, дабы заполнить ими резюме.

По-мне это порочная практика - оптимизировать говнокод в оптимальный код.

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

Он выполняет набор математических преобразований программы, каждое из которых само по себе элементарно. (Оно может быть неэлементарным в смысле реализации в коде компилятора, но в том, что оно собой представляет по смыслу – вполне).

Начиная с самых базовых трансформаций: продвижение констант, устранение лишних переменных, устранение общих подвыражений и т.п.

Просто раньше таких трансформаций компиляторы делали мало и плохо, а теперь делают много и хорошо. И все подводные камни, заложенные в семантику языка, вылезли на поверхность.

Я считаю, что проблему нужно решать именно на уровне спецификации языка.

Насколько я знаю, в крестах такие подвижки есть, и там часть терминологии undefined behavior заменяют на erroneous behavior.

«erroneous behavior - The (incorrect) behavior that the implementation is recommended to diagnose. »

Просто пока до комитетчиков что-то доходит, обычно много воды утекает.

Конкретно про арифметику знаковых чисел — я считаю, что она не должна быть UB. Это должно быть определённое поведение, даже если оно implementation-defined.

Пусть компилятор может относиться к числам как к числам в математическом смысле только в тех фрагментах программы, где он может ДОКАЗАТЬ отсутствие переполнений.

Вот тогда работа компилятора будет такой, как хочет firkax.

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

Нет, тормозит не поэтому. Это никак не связанные вещи.

Тормозит потому, что быстро писать тормозящий код экономически выгодно, ведь за него платят. А медленно писать оптимальный – выгодно крайне редко. Там, где выгодно, там тоже его пишут. Но не часто и мало, под потребности рынка.

Что там награфоманили какие-то теоретики тут совершенно не важно

Для кого не важно?

Разрабы компилятора делают именно так, как награфоманили теоретики.

И это – факт реальности, с которым надо считаться. Другого языка Си и других компиляторов у нас нет.

Оно не равноценно потому что систематически даёт разный результат работы программы.

С точки зрения теоретиков, оба варианта такой программы (с оптимизациями и без) — некорректная программа. Поэтому какие именно результаты даёт некорректная программа, совсем не важно. Это лежит за областью ответственности компилятора.

Ну насчёт генерации раздутого кода я хз, по-моему компиляторы С страшно умные и если они и генерируют раздутый код, значит так надо.

Что им дали на вход, то и генерируют. Проблема же не в компиляторах, а в том, что собой представляет исходный код.

Кресты и Раст — это куча высокоуровневых абстракций, которые при компиляции каждый раз разворачиваются в огромные блоки машинного кода.

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