gds 18.03.2013 11:44 umodniA63A5C27

Наша редакция рада ответить на просьбу господина @ulidtko, изложенную в http://amd63.psto.net/tsfgse#123 , нижеследующим куском кода: https://gist.github.com/gdsfh/7140f41aca...
Там в каментах я показал, во что экстрактится всё это безобразие. Как обычно, все пруф-термы стёрты, остались только рантайм-значения.
Если будут какие-либо вопросы — отвечу на них в этом итт треде.

coq, cs, fp, it, ocaml
Recommended by:

@komar: популяризация петушиного языка в этом ITT треде

and @4da, @kb
1. amd63 18.03.2013 11:59 Azoth

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

2. gdsamd63 /1 18.03.2013 12:08

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

писал на 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.

Do you really want to delete ?