Читаю презентацию Ксавье Лероя.
Programming a compiler with a proof assistant: an experience report (invited talk), Xavier Leroy (INRIA, Paris-Rocquencourt).
У них ушло 2 с половиной человеко-года на 40000 строк кода (Coq) оптимизирующего компилятора из подмножества Си в ассемблер PowerPC, с доказательством корректности.
На страничке 52 там приводится следующая табличка:Зависимый абстрактный тип данныхЗависимо типизированная монадаНеобходимо доказывать свойствадля каждой операции над абстрактным типомдля каждой операции над монадами, включая return и bindСвойства распространяютсядля всех прошедших проверку типов вычисленийдля любых монадических операцийТо есть, с монадами получается меньше возни.
Coq на моем маке не заводится. :(
У них ушло 2 с половиной человеко-года на 40000 строк кода (Coq) оптимизирующего компилятора из подмножества Си в ассемблер PowerPC, с доказательством корректности.
На страничке 52 там приводится следующая табличка:Зависимый абстрактный тип данныхЗависимо типизированная монадаНеобходимо доказывать свойствадля каждой операции над абстрактным типомдля каждой операции над монадами, включая return и bindСвойства распространяютсядля всех прошедших проверку типов вычисленийдля любых монадических операцийТо есть, с монадами получается меньше возни.
Coq на моем маке не заводится. :(