Правильно ли такому нубасу как я представляется, что ты написал код на Coq чтобы он тебе сгенерировал такой код на Ocaml (main + input_list_int) которому присуще доказанное нечто, не присущее тем же main + input_list_int но написанными сразу руками на Ocaml без использования Coq? И что те куски, которые тебе очень сильно "важны", ты будешь всегда генерить Coq-ом а не писать прямо на Ocaml-е руками?

#tsiezf/1

reply

не полностью распарсил, поэтому уточню:

писал на coq код, содержащий работу как с рантайм-значениями, так и с доказательствами.

работать код будет одинаково в coq и в окамле. (но конкретно тут — не совсем, так как в coq не получится реализовать монадные функции. в остальном же — код работает одинаково.)

при экстракции стираются все пруфы. Они принадлежат "сорту" Prop. Например, { r : list A | length r = sz } содержит в себе как computational term (list A), так и proof term ("length r = sz"). Пруф-терм стирается, в результате vec n A эквивалентно list A, и экстрактится в " 'a list " в окамле.

доказательства я писал руками.

доказательств нет в рантайме.

куски кода, где нужны какие-то гарантии, я часто пишу на coq.

кроме того, на coq пишу куски кода, где системы типов окамла не хватает (либо требуются ональные извращения Олег-стайл). Такой код экстрактится в окамл-код, содержащий вызовы модуля Obj — небезопасное изменение типов значений. За ручное использование Obj нужно отрывать руки, а автоматическое, проверенное coq'ом — вполне ок. Почему Obj — да потому что системы типов не хватает, в этом-то и суть данного применения coq.

#tsiezf/2

reply