Здравствуйте, Sinclair, Вы писали:
S>А что, CoQ каким-то волшебным образом угадает намерения программиста, и сможет доказывать корректность неаннотированных программ?
Нет, конечно. Просто CoQ это и не завтипы прямо в бизнес-логике, но и не пре- и пост-условия.
Re[8]: Idris 2 vs Clojure. Для чего нужен (ли) Idris 2 в индустриальном коде?
Здравствуйте, cppguard, Вы писали:
C>Нет, конечно. Просто CoQ это и не завтипы прямо в бизнес-логике, но и не пре- и пост-условия.
Надо почитать. Найти бы время ещё на это всё...
Уйдемте отсюда, Румата! У вас слишком богатые погреба.
Re[9]: Idris 2 vs Clojure. Для чего нужен (ли) Idris 2 в индустриальном коде?
Здравствуйте, Sinclair, Вы писали:
S>Найти бы время ещё на это всё...
И не говорите...
Я как-то открыл свой список "что бы хотел поизучать" и понял, что не менее половины просто уже не имеет смысла...
