только пруфы. Потому что слишком легко налажать и сделать фигню, которая чекается, но работает неправильно. И это в языке с завтипами
Вот нафига хаскелю тактики?
Ну там язык описания тактик не совсем хорош , но в целом точку зрения разделяю
а где в Хаскеле тактики?
Ltac2 уже ближе к полноценному PL
https://coq.inria.fr/refman/proof-engine/ltac2.html
Выше ссылку кидали, Сэнди Магваер делает
В самом языке тактик завтипов нет
Ну понятное дело я не про это Код, который выдают тактики, ненадежный, его надо проверять. Завтипы отлично проверяют пруфы, потому что их содержание не особо важно, а вот программы проверяют не очень хорошо Т. е. в хаскелле скорее всего придётся к тактикокоду неизбежно писать тесты, а кому это нафиг надо
Обсуждают сегодня