Можно ли писать программы на C, используя Coq?
Я знаю, что можно извлечь программы Coq в программы на Haskell и OCaml. Есть ли способ сделать это с C?
Я представляю библиотеку, которая моделирует язык Си. Возможно, такая библиотека будет содержать коллекцию аксиом о том, как конструкции C взаимодействуют с памятью процесса, а также аксиомы и теоремы о числах с плавающей запятой IEEE. Тогда он сможет построить C-программу в Coq вместе с теоремами о программе.
Я бы использовал такую библиотеку, скажем, для построения алгоритма быстрой сортировки C, который работает с массивами чисел с плавающей точкой, которые будут компилироваться GCC.
2 ответа
C недоступен в качестве цели извлечения для программ Coq; поддерживаются только OCaml и Haskell. Тем не менее, мы все еще можем использовать Coq для написания проверенного программного обеспечения на C: например, Verified Software Toolchain позволяет нам переводить программы на C в формат, понятный Coq, и доказывать теоремы об их поведении. Обратите внимание, что эти доказательства имеют другой вид, чем вы могли бы использовать, если вы сделали какие-либо доказательства о программах Coq, потому что программа C просто конвертируется в свое синтаксическое дерево как тип данных Coq вместо функции Coq.
Появилась новая глава Software Foundations , в которой рассматриваются практические аспекты взаимодействия Coq и C.