CD
Если он верифицирован, то будет естественно соблюдать.
Компилятор Idris верифицирован?
Size: a a a
2020 August 24
EG
Компилятор идрис написан на хаскелле, начнём с этого
p
Компилятор Idris верифицирован?
Хз, какое это имеет отношение к делу?
p
Компилятор идрис написан на хаскелле, начнём с этого
На идрисе
CD
Хз, какое это имеет отношение к делу?
Ну где ты взял формально верифицированный компилятор
p
Ну где ты взял формально верифицированный компилятор
Ещё раз, какое это отношение имеет к разговору?
CD
Что-то я не помню формальную верификацию над LLVM
CD
Ещё раз, какое это отношение имеет к разговору?
Простое - твоя верификация работает хуже тестов
CD
Тесты не нашли злонамеренную ошибку в коде
EG
На идрисе
Угу, компилятор Idris 2 на Idris
p
Простое - твоя верификация работает хуже тестов
Не вижу свчзи
EG
А компилятор Idris на Haskell
CD
Не вижу свчзи
А верификация не нашла случайную ошибку
EG
А Haskell на C
EG
А C на C
EG
А C на C
CD
Так что после верификации достаем 1000%-ные тесты
EG
Проверифицировать всех черепах до самого низа возможным не представляется
CD
И узнаём сколько интересных багов бывает в gcc или delphi 7
CD
вида if (input == 228) panic!();