История изменений
Исправление no-such-file, (текущая версия) :
даже если это сишечка
В сишечке типы используются не для доказательства корректности. Какие-то выводы про корректность это побочный эффект и целиком инициатива современных компиляторов. Можно сделать компилятор сишечки без проверок корректности.
оптимизирующие компиляторы
Какое отношение оптимизация имеет к проверке корректности? Те же современные компиляторы сишечки и крестов кладут жирный болт на корректность при оптимизации ибо УБ. Да и в растишке нет-нет да и пихнут unsafe ради скорости.
железо с которого ты это пишешь верифицировано какими-нибудь Agda-ми и Сoq-ми
Обрати внимание, железо верифицировано не каким-нибудь verilog-ом, а сторонними инструментами. Я совершенно не против статических анализаторов кода и других подобных систем анализа. Но они работают в целом без привязки к типам именно языка (хотя и могут учитывать эту информацию, если она имеется), используя различные связи в коде, в том числе выходящие за рамки языка как такового (паттерны, стили, стороннее описание бизнес-логики и т.п.).
Исправление no-such-file, :
даже если это сишечка
В сишечке типы используются не для доказательства корректности. Какие-то выводы про корректность это побочный эффект и целиком инициатива современных компиляторов. Можно сделать компилятор сишечки без проверок корректности.
оптимизирующие компиляторы
Какое отношение оптимизация имеет к проверке корректности? Те же современные компиляторы сишечки и крестов кладут жирный болт на корректность при оптимизации ибо УБ. Да и в растишке нет-нет да и пихнут unsafe ради скорости.
железо с которого ты это пишешь верифицировано какими-нибудь Agda-ми и Сoq-ми
Обрати внимание, железо верифицировано не каким-нибудь verilog-ом, а сторонними инструментами. Я совершенно не против статических анализаторов кода и других подобных систем анализа. Но они работают в целом без привязки к типам именно языка (хотя и могут использовать эту информацию, если она имеется), используя различные связи в коде, в том числе выходящие за рамки языка как такового (паттерны, стили, стороннее описание бизнес-логики и т.п.).
Исходная версия no-such-file, :
даже если это сишечка
В сишечке типы используются не для доказательства корректности. Какие-то выводы про корректность это побочный эффект и целиком инициатива современных компиляторов. Можно сделать компилятор сишечки без проверок корректности.
оптимизирующие компиляторы
Какое отношение оптимизация имеет к проверке корректности? Те же современные компиляторы сишечки и крестов кладут жирный болт на корректность ибо УБ. Да и в растишке нет-нет да и пихнут unsafe ради скорости.
железо с которого ты это пишешь верифицировано какими-нибудь Agda-ми и Сoq-ми
Обрати внимание, железо верифицировано не каким-нибудь verilog-ом, а сторонними инструментами. Я совершенно не против статических анализаторов кода и других подобных систем анализа. Но они работают в целом без привязки к типам именно языка (хотя и могут использовать эту информацию, если она имеется), используя различные связи в коде, в том числе выходящие за рамки языка как такового (паттерны, стили, стороннее описание бизнес-логики и т.п.).