А его потом, по-моему, кто-то про ptn спросил в кулуарах. Но могу ошибаться, я в тот день страшно не выспался, весь день как в тумане прошёл, вырубало просто адски.
O, а я смотрю, имя знакомое, но какой ник за ним скрывается не вспомнил. :) Как обзор инструментов доклад неплохой получился. Что до Идриса... он наверно не для этого, там все же другие задачи решаются. Не показать равенство двух хаскельных функций, а заимплементить одну так, чтобы в ее типе выразить какие-то нужные свойства. При этом выглядеть она наверняка будет совсем не так, как результат у Гиббонса.
Спасибо! Хотя обзор инструментов постольку поскольку, поэтому очень ограниченный.
Строго говоря, когда стал доказывать на Isabelle, я тоже перестал доказывать свойства ф-ий Haskell, поскольку в Isabelle семантика ф-ий отличается (тотальность, eager vs. lazy) - просто потом экстракцию в Haskell делаю.
В Idris (как и Agda) с недавних пор завезли equational-style theorem proving, поэтому можно повторить результат относительно близко.
Кроме того, хотел пожаловаться на заголовок поста: то как я дурю людей к использованию theorem prover'а отношения не имеет. Получается fooling people and using theorem prover. :D
Comments 5
Reply
Reply
Reply
Как обзор инструментов доклад неплохой получился.
Что до Идриса... он наверно не для этого, там все же другие задачи решаются. Не показать равенство двух хаскельных функций, а заимплементить одну так, чтобы в ее типе выразить какие-то нужные свойства. При этом выглядеть она наверняка будет совсем не так, как результат у Гиббонса.
Reply
Строго говоря, когда стал доказывать на Isabelle, я тоже перестал доказывать свойства ф-ий Haskell, поскольку в Isabelle семантика ф-ий отличается (тотальность, eager vs. lazy) - просто потом экстракцию в Haskell делаю.
В Idris (как и Agda) с недавних пор завезли equational-style theorem proving, поэтому можно повторить результат относительно близко.
Кроме того, хотел пожаловаться на заголовок поста: то как я дурю людей к использованию theorem prover'а отношения не имеет. Получается fooling people and using theorem prover. :D
Reply
Leave a comment