«Program Definition» в последних версиях Coq - это ацкая силища.
В двух словах, они позволяют писать сертифицированные программы как обычные, т.е. как будто бы доказательный компонент отсутствует (например, использовать {x:nat | even x} как будто это просто nat), а затем автоматически пытается решить все оставшиеся «обязательства»; те, что не
(
Read more... )