тесты -- затем, чтобы проверить, правильную ли я модель накодил для доказательств. Ну да всё равно тестировал производительность, там и корректность заодно проверил.
Если бы меня не попросили проверить, есть ли смысл в "умной буферизации" по производительности, я бы не лепил тесты, проверил бы потом, в деле.
А наоборот -- если есть тесты, полные, исправляемые при каждом изменении функциональности, то доказательства не нужны. Если же исправлять их лень, или нет гарантий полноты тестов, то есть смысл подумать о доказательствах.
Если же исправлять их лень, или нет гарантий полноты тестов, то есть смысл подумать о доказательствах. Да, но может же ведь быть ошибка и в модели, которая, как обычно, будет именно в том месте, для которого было лень переделывать тесты?
1. в моделях ошибок обычно сильно меньше. 2. в случае доказательств я уверен: как бы ни менялся код, доказательства будут постоянно отражать факты о коде. В случае тестов таких гарантий никто не даст, там надо морочиться с test coverage всяким.
ну хорошо, как бы ты подошёл к решению этой задачи (а именно, "реализовать и доказать императивный алгоритм")? Свести его к потоку блоков -- не очень-то вариант. Ещё идеи?
Сперва поразился числу строк, а потом смотрю - там каждый аргумент на отдельной строке. Зачем так?
В целом прикольно, вспомнился ATS, где любой ввод-вывод практически в такую вот штуку выливается, и встроенный решатель целочисленный как раз на такие задачки хорошо заточен. Только, не зная кока, складывается впечатление, что это все write-only, и что никто кроме автора (и тот лишь в интервале сегодня - две недели спустя) в этом не разберется.
да, в некоторых местах можно было бы и в одну строку записать. А так -- в случаях, когда предметная область не близка, я предпочитаю предельную структурированность и ясность кода, чтобы связь выравнивания и ast была как можно более явной. А текущая задача была пока не близкой мне.
Про "не разберётся" -- разберётся ещё как. В типах, сигнатурах и телах функций уж точно. А пруфы -- так, хуйня из-под коня, в которой разбираться особо не нужно. А в окамловском коде разбираться и не нужно -- это всего лишь результат трансляции.
Comments 12
Reply
Если бы меня не попросили проверить, есть ли смысл в "умной буферизации" по производительности, я бы не лепил тесты, проверил бы потом, в деле.
А наоборот -- если есть тесты, полные, исправляемые при каждом изменении функциональности, то доказательства не нужны. Если же исправлять их лень, или нет гарантий полноты тестов, то есть смысл подумать о доказательствах.
Reply
Да, но может же ведь быть ошибка и в модели, которая, как обычно, будет именно в том месте, для которого было лень переделывать тесты?
Reply
2. в случае доказательств я уверен: как бы ни менялся код, доказательства будут постоянно отражать факты о коде. В случае тестов таких гарантий никто не даст, там надо морочиться с test coverage всяким.
Reply
Reply
Кажется мне, что ты как-то слишком сложно делаешь.
Нутром это чую, но доказать не могу (c)
Reply
Reply
Ладно. Сойдёмся на том, что сложность состоит в разнице мышления между нами ;-)
Reply
Reply
В целом прикольно, вспомнился ATS, где любой ввод-вывод практически в такую вот штуку выливается, и встроенный решатель целочисленный как раз на такие задачки хорошо заточен. Только, не зная кока, складывается впечатление, что это все write-only, и что никто кроме автора (и тот лишь в интервале сегодня - две недели спустя) в этом не разберется.
Reply
Про "не разберётся" -- разберётся ещё как. В типах, сигнатурах и телах функций уж точно. А пруфы -- так, хуйня из-под коня, в которой разбираться особо не нужно. А в окамловском коде разбираться и не нужно -- это всего лишь результат трансляции.
Reply
Leave a comment