История изменений
Исправление Stanson, (текущая версия) :
Так доказательство кода как раз такой баг пропустит, потому что для него верно работающий процессор и компилятор входят в аксиоматику.
Нет. Процессор это тоже код, нынче. Verilog какой-нибудь. А компилятор для таких штук не обязательно должен быть gcc, или тем более llvm которые доказать практически нереально. Вполне достаточно какого-нибудь tcc или ещё более простой штуки. Кроме того, для простые ответственные вещи типа sin() можно вообще на ассемблере написать исключив компилятор вообще. Кстати, вот ассемблер вполне можно полностью протестировать как раз этими самыми тестами.
Так что доказать код нынче вполне реально начиная с железа. Ну это если действительно нужна гарантия качества, а не модные термины.
Исправление Stanson, :
Так доказательство кода как раз такой баг пропустит, потому что для него верно работающий процессор и компилятор входят в аксиоматику.
Нет. Процессор это тоже код, нынче. Verilog какой-нибудь. А компилятор для таких штук не обязательно должен быть gcc, или тем более llvm которые доказать практически нереально. Вполне достаточно какого-нибудь tcc или ещё более простой штуки. Кроме того, для простые ответственные вещи типа sin() можно вообще на ассемблере написать исключив компилятор вообще. Кстати, вот ассемблер как раз вполне можно полностью протестировать как раз этими самыми тестами.
Так что доказать код нынче вполне реально начиная с железа. Ну это если действительно нужна гарантия качества, а не модные термины.
Исправление Stanson, :
Так доказательство кода как раз такой баг пропустит, потому что для него верно работающий процессор и компилятор входят в аксиоматику.
Нет. Процессор это тоже код, нынче. Verilog какой-нибудь. А компилятор для таких штук не обязательно должен быть gcc, или тем более llvm которые доказать практически нереально. Вполне достаточно какого-нибудь tcc или ещё более простой штуки. Кроме того, для простые ответственные вещи типа sin() можно вообще на ассемблере написать исключив компилятор вообще. Кстати, вот ассемблер как раз вполне можно полностью протестировать этими самыми тестами.
Так что доказать код нынче вполне реально начиная с железа. Ну это если действительно нужна гарантия качества, а не модные термины.
Исходная версия Stanson, :
Так доказательство кода как раз такой баг пропустит, потому что для него верно работающий процессор и компилятор входят в аксиоматику.
Нет. Процессор это тоже код, нынче. А компилятор для таких штук не обязательно должен быть gcc, или тем более llvm которые доказать практически нереально. Вполне достаточно какого-нибудь tcc или ещё более простой штуки. Кроме того, для простые ответственные вещи типа sin() можно вообще на ассемблере написать исключив компилятор вообще. Кстати, вот ассемблер как раз вполне можно полностью протестировать этими самыми тестами.
Так что доказать код нынче вполне реально начиная с железа. Ну это если действительно нужна гарантия качества, а не модные термины.