История изменений
Исправление AndreyKl, (текущая версия) :
Круто, должно работать. Но твой способ единственный в данном случае. Никуда не денешься, так тоже бывает.
Кстати, что делать с доказательной проверкой, когда текст функции на Coq и текст изначальной проверяемой функции на Си++ или Ocaml не совпадают? Ведь тоже может получиться, что проверили не то, что дано, а то, что предположительно поняли.
Заворачивать исходный текст в монаду в целью чтобы текст совпадал практически полностью.
Желательно иметь автоматическую трансляцию, как вот тут например https://github.com/formal-land/coq-of-rust
Исходная версия AndreyKl, :
Кстати, что делать с доказательной проверкой, когда текст функции на Coq и текст изначальной проверяемой функции на Си++ или Ocaml не совпадают? Ведь тоже может получиться, что проверили не то, что дано, а то, что предположительно поняли.
Заворачивать исходный текст в монаду в целью чтобы текст совпадал практически полностью.
Желательно иметь автоматическую трансляцию, как вот тут например https://github.com/formal-land/coq-of-rust