Да, скорее, это система для доказательств, но там делается упор на конструктивную математику. Есть Extraction Language для Ocaml, Haskell, Scheme и какой-то его (CoQ) внутренний язык Toplevel.
Программирование выглядит типа того, что формулируешь спецификацию, потом детализируешь её, некоторые куски дописываешь сам, потом к спецификации добавляешь упрощающие доказательство мелочи, и после некоторых мучений получаешь программу, которая гарантированно соответствует спецификации. Вообще, мучения на практике возникают, в основном, только при доказательстве всяческих (не)равенств, во многом остальном выглядит похожим на Epigram. Вроде бы, чего-то в Epigram2 в делают с (не)равенствами в их Observational Type System.
Сложность доказательства зависит, главным образом, от сложности поставленных условий. Например, бывает просто упорядочивающая перестановка, а бывает ещё и с дополнительными условиями, например, видел статью, где в CoQ описывалась пирамидальная сортировка. Можно сформулировать задачи минимизации, только оно далеко не все их них сможет разрешить самостоятельно.
Конечно, это не похоже на языки общего назначения, но могло бы быть таким, при условии полной автоматизации доказательств. Так что, ИМХО, не многое отделяет proof assistant'ы от языков программирования общего назначения.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2008-01-20 12:59 pm (UTC)но там делается упор на конструктивную математику.
Есть Extraction Language для Ocaml, Haskell, Scheme
и какой-то его (CoQ) внутренний язык Toplevel.
Программирование выглядит типа того,
что формулируешь спецификацию, потом
детализируешь её, некоторые куски
дописываешь сам, потом к спецификации
добавляешь упрощающие доказательство мелочи,
и после некоторых мучений получаешь программу,
которая гарантированно соответствует спецификации.
Вообще, мучения на практике возникают, в основном,
только при доказательстве всяческих (не)равенств,
во многом остальном выглядит похожим на Epigram.
Вроде бы, чего-то в Epigram2 в делают с
(не)равенствами в их Observational Type System.
Сложность доказательства зависит, главным образом,
от сложности поставленных условий.
Например, бывает просто упорядочивающая перестановка,
а бывает ещё и с дополнительными условиями, например,
видел статью, где в CoQ описывалась пирамидальная сортировка.
Можно сформулировать задачи минимизации, только оно
далеко не все их них сможет разрешить самостоятельно.
Конечно, это не похоже на языки общего назначения, но могло бы
быть таким, при условии полной автоматизации доказательств.
Так что, ИМХО, не многое отделяет proof assistant'ы
от языков программирования общего назначения.