В чем разница между худой, f* и dafny?
Они из Microsoft и кажутся помощниками? Помимо синтаксических различий, есть ли практические аспекты, которые отличают их друг от друга (например, способность делать автоматизацию, выразительную силу и т. Д.)? Я новичок в формальной проверке.
Редактировать: я не спрашиваю, какой из них лучше, я просто заинтересован в техническом сравнении между различными функциями, предлагаемыми этими инструментами. Я ищу что-то подобное
1 ответ
Каждый инструмент имеет уникальный дизайн, он создан и подвержен влиянию разных людей с разными целями и принципами, но все авторы являются друзьями и сидят в нескольких офисах друг друга на протяжении многих лет.
Растан Лейно разработал Dafny как преемник многих систем, которые он создавал прежде, включая ESC Java и SpeC#.
Dafny основан на императивном языке, подобном Java или C#, с возможностью писать инварианты состояний логического стиля Hoare, что позволяет пользователям языков проверять свойства методов и объектов, которые используют изменяемое состояние, циклы, массивы и т. Д. Основная теория Дафни - это логика пользовательской программы, в основном разработанная Растаном и несколькими сотрудниками. Dafny выполняет условия проверки, которые он генерирует, компилируя их в промежуточный язык проверки Boogie, который, в свою очередь, компилирует их в запросы, которые передаются в SMT-решатель, например Z3 или CVC4, для выполнения.
Цель Dafny в том, чтобы чувствовать себя очень похожим на императивные объектно-ориентированные языки, которые знакомы пользователям с дополнительной возможностью проверки ваших программ.
F* основан на новой теории типов, разработанной Nikhil Swamy и соавторами, он начинался как ML-подобный язык программирования с добавлением уточняющих типов, которые были выпущены в стиле Dafny, но существенно изменился за последние несколько лет из-за многочисленные внешние дополнения, а также влияния Дафни, Лин, Ликвида Хаскелла и так далее.
F* также переводит свои условия проверки в SMT-решатели, такие как Dafny, но не использует промежуточный язык проверки, такой как Boogie. F* недавно получил способность использовать тактику, находящуюся под сильным влиянием языка тактики Lean.
Основным нововведением F* по сравнению с такими инструментами, как Dafny и другими уточняющими типами, является использование Dijkstra Monads способа описания "эффекта" кода, позволяющего конструктору эффектов контролировать сгенерированные условия проверки. DM позволяют пользователям рассуждать на разных уровнях, например, код в Pure Эффект не может использовать состояние или генерировать исключения, а пользователь может игнорировать эффективные функции, которые они не используют.
На дизайн Лин сильно влияют Coq и другие интенсиональные теории типов, и он во многом похож на них. Цель Лин - объединить лучшие автоматизированные и интерактивные средства доказательства теорем, привнося методы из автоматизированного мира (SMT) в теорию типов. Мир. Он обладает очень мощными возможностями метапрограммирования и все больше и больше автоматизируется. Lean не требует решения SMT и переопределяет многие из основных процедур специализированным способом для теории типов Lean.
Вы можете рассматривать F* и Lean как прикрывающие схожие пространства, но подчеркивая различные способы их достижения.
Я с удовольствием уточню больше, если это не прояснит.
Источник: основной разработчик Lean, разработчик F*, а иногда пользователь и участник Dafny, проработавший в MSR ~7 месяцев и лично знакомый со всеми авторами инструмента.