МБ
Так LaTTe идеологически сделан.
Size: a a a
2020 March 16
AT
Ну, да... Ужа с ежом плохо получается скрещивать. Typed Racket вот довольно... Ну. Костыльный местами. Но я себе мыслю нечто типа такого. Есть базовый динамический язык, и мы не делаем его типизированным, но в некотором DSL можем доказывать свойства отдельных функций.
А на чём тогда основывать доказательства свойств функций?
МБ
А на чём тогда основывать доказательства свойств функций?
На вот этом самом LaTTe, он извлекает функции свои в Plain Clojure.
AT
На вот этом самом LaTTe, он извлекает функции свои в Plain Clojure.
Т.е. получается чистый типизированный DSL, который экстрактится в нетипизированный язык? Типа как Gallina? 😉
PS
Имеются в виду формальные доказательства? А есть примеры?
А что здесь особенного? Вот пример с использованием любимого многими тут Coq :)
A Verified LL(1) Parser Generator
https://drops.dagstuhl.de/opus/volltexte/2019/11079/pdf/LIPIcs-ITP-2019-24.pdf
A Verified LL(1) Parser Generator
https://drops.dagstuhl.de/opus/volltexte/2019/11079/pdf/LIPIcs-ITP-2019-24.pdf
МБ
А что здесь особенного? Вот пример с использованием любимого многими тут Coq :)
A Verified LL(1) Parser Generator
https://drops.dagstuhl.de/opus/volltexte/2019/11079/pdf/LIPIcs-ITP-2019-24.pdf
A Verified LL(1) Parser Generator
https://drops.dagstuhl.de/opus/volltexte/2019/11079/pdf/LIPIcs-ITP-2019-24.pdf
Спасибо
МБ
8000 строк кода для LL(1)...
AT
На тему парсинга есть еще Validating LR(1) Parsers: http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validating-parsers.pdf
PS
8000 строк кода для LL(1)...
Но это не отменяет того факта, что формальные спецификации в построении компиляторов используются достаточно широко. Возможность писать код прямо на высокоуровневом языке спецификации, на мой взгляд, гораздо ценнее, чем возня с зависимыми типами и проч. А для доказательств, как уже говорилось выше, у компиляторщиков есть те же SMT-решатели с Datalog.
PS
На тему парсинга есть еще Validating LR(1) Parsers: http://gallium.inria.fr/~fpottier/publis/jourdan-leroy-pottier-validating-parsers.pdf
В related work эта статья есть :)
AT
стоило ожидать)
RS
По поводу длины доказательства Н.Н.Непейвода утверждает, что доказательство должно быть не более чем в три раза длиннее программы: http://900igr.net/up/datas/207437/060.jpg
МБ
А где об этом можно прочитать?
МБ
Это Теорема Оревкова, кажется. Но я её так и не нашёл.
EZ
Rifat S
По поводу длины доказательства Н.Н.Непейвода утверждает, что доказательство должно быть не более чем в три раза длиннее программы: http://900igr.net/up/datas/207437/060.jpg
Это не то что там написано
RS
Непейвода Н.Н. Прикладная логика ISBN 5-7615-0490-1
DS
Rifat S
Непейвода Н.Н. Прикладная логика ISBN 5-7615-0490-1
А какова общая идея доказательства этой теоремы?
Звучит любопытно
Звучит любопытно
IJ
Rifat S
Непейвода Н.Н. Прикладная логика ISBN 5-7615-0490-1
Так давайте ему напишем, он отвечает на письма
МБ
Готов подписать письмо :)
A
Это не то что там написано
+