DF
фм ето што
Size: a a a
2021 July 07
DF
спасибо да тема интнресная
LO
путин не Тит
DF
если не путин то тит
BK
хорошо бы что-то уже ближе к непосредственно описанию и теории фм
статья и тредик хорошие, но статью я еще не досмотрел, пока читаю скорее про применение
статья и тредик хорошие, но статью я еще не досмотрел, пока читаю скорее про применение
AG
нет единой теории
AG
принято считать что фм это "спектр"
AG
от тестирования с элементами статистического анализа до теорем
AG
собственно если чуть углубить разделение на лёгкие и тяжелые, получится три группы
AG
продвинутые тесты, модели и теоремы
AG
ну и в каждой свой набор методов и теорий
AG
начинается всё с ключевой идеи о спецификации
AG
типа есть программный артефакт, а есть какое то приближенное описание, и мы хотим с той или иной степенью строгости сопоставить одно другому
AG
то есть тесты это какие-то кусочные но детальные спецификации, проверяемые автоматически, модели - более полные и приближенные, опять же автопроверямые, ну и теоремы - наиболее полные, но не автоматизируемые в общем случае
AG
детальность теорем в пределе приводит к полному слиянию с программами, это и есть изоморфизм карри-говарда
BK
это понятно, я не так выразился, скорее имел в виду что-нибудь по имплементации, т.е. то что вы дальше описываете
LO
можешь пока заняться настройкой coq под VSCode
BK
прииерно понял!
BK
о боже