Полностью формально верифицируемый код на сильном языке может не все. Таким образом, реализацию все равно пришлось бы делать на менее сильном языке, где уже можно допустить ошибки.
код может вполне многое, почти всегда достаточное для реальных применений. Все шаги трансляции высокоуровневого кода тоже могут быть формально проверены, вплоть до микросхемок.
это слишком сложно и ненадёжно, как раз из-за непроверяемых частей. Я бы сделал, например, dsl на coq с доказанной трансляцией в машинный код, имеющий заданную семантику, проверенную при изготовлении процессора.
зато в dsl бесконечная рекурсия возможна. Далее, например, возможно использовать коиндуктивные типы данных для представления состояния, и через подходы, подобные бисимуляции, доказывать эквивалентность программ до и после компиляции. Ну или как-то ещё сделать — я пока не просифуанал, я только учусь. Но то, что это возможно — не сомневаюсь, хотя бы из-за существования CompCert (проверенного почти-сишного компилятора).
7 comments
recommend
bookmark
subscribe
видео не смотрел, но порицаю: в разные железяки, особенно в подобные, нужно заливать только формально-проверенный код.
Полностью формально верифицируемый код на сильном языке может не все. Таким образом, реализацию все равно пришлось бы делать на менее сильном языке, где уже можно допустить ошибки.
код может вполне многое, почти всегда достаточное для реальных применений. Все шаги трансляции высокоуровневого кода тоже могут быть формально проверены, вплоть до микросхемок.
на каком языке? трансляция agda→haskell плюс дописывание непроверяемых частей?
это слишком сложно и ненадёжно, как раз из-за непроверяемых частей. Я бы сделал, например, dsl на coq с доказанной трансляцией в машинный код, имеющий заданную семантику, проверенную при изготовлении процессора.
хм, в coq же нет бесконечной рекурсии, как вы сделаете простую циклограмму, например?
зато в dsl бесконечная рекурсия возможна. Далее, например, возможно использовать коиндуктивные типы данных для представления состояния, и через подходы, подобные бисимуляции, доказывать эквивалентность программ до и после компиляции. Ну или как-то ещё сделать — я пока не просифуанал, я только учусь.
Но то, что это возможно — не сомневаюсь, хотя бы из-за существования CompCert (проверенного почти-сишного компилятора).