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

[gds]

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

Comments

[plumqqz]

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

[gds]

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

[plumqqz]

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

[gds]

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

[thedeemon]

Фигасе простыня, я ничего не понял.
В коке разве нет уже готового вектора? Хрестоматийный же тип из всех учебников по завтипам.

Ну и это, зачем ты туда волосы засовывал?

[gds]

простыня -- да. Но было интересно, получится ли у меня строить computational terms через тактики destruct, exists, refine/exact (которые отсебятины не допускают), доказывая остальное любыми доступными средствами, в том числе тактиками, как С-тона на душу положит.

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

[thedeemon]

То, что тактиками можно написать правильно, еще не показывает, что нельзя неправильно. Я ж тоже потом показал правильный вариант с тактиками на идрисе.

[gds]

так тут цимес в том, что тактики не могут никак изменить тело, предоставленное через destruct, exists, refine, exact, и я считаю, что так гораздо более ошибкозащищённо: если уж явно / почти явно предоставил тело, значит о чём-то кагбэ намекал, в стиле "я лучше знаю, как оно должно вычисляться, а доказательства сейчас налепим".