построение термов тактиками в coq -- безопасно

[gds]

Сегодня thedeemon показал ужосы, от которых у меня волосы в жилах стынут.
А мне стало интересно, можно ли накосячить подобным образом в coq.
Но писал я быстро, поэтому код некрасивый. Например, можно спокойно попрятать многое в implicit arguments, да и для vec выбрать более кошерный тип (например, кошерный в плане strict positivity).

Comments

[plumqqz]

"Мы, мерзавцы, думали, что нам эта комиссия поможет. Ни хрена она нам не помогла!"
Вообще, зачем вы всем этим занимаетесь?

[gds]

сейчас, например, для статически-проверяемых миграций схем реляционных баз данных. Так, чтобы после накатывания изменений в виде ddl и редкого sql всё, работавшее ранее, продолжало работать, кабута ничо не было. И чтобы функции на plpgsql не вызывали тупых ошибок выполнения -- тех, которые можно исключить статически. (конечно, остаются те, которые исключить нельзя, но на моей практике их относительно немного.)

[plumqqz]

Извините, но приведенный пример лично меня убеждает лишь в том, что в случае примения этой методики было затрачено очень много усилий и только.
По-моему, это должно быть ясно и вам.

[gds]

не надо "извините", Вы правы абсолютно.
Тем не менее, иногда гарантии стоят усилий, особенно совершаемых однократно.
Другие способы показательства (увы, не доказательства) корректности состоят в поднятии тестовой БД и прогонке на ней кучи тестов, что требует примерно "O(объём функциональности)" операций, тогда как в моём случае получается приблизительно "O(1) + однократные усилия". А я весьма много пишу с использованием реляционок, мне они нравятся, аж мимими. Поэтому решил поставить на второй вариант -- первый вариант остопиздел за долгий десяток лет разработки с использованием реляционок.
Кроме того, тесты всё не покрывают, и тесты надо изменять с изменением функциональности, тогда как процедура доказательства корректности в простых случаях является автоматической, не требует вмешательства.

[nivanych]

"Лучше бы водку пили, в самом деле, чем совершали эти однократные усилия...", - сказал Крокодил.