История изменений

Злобный матан, однако. Ты это всё вручную писал? У меня ощущение, что написать доказательство на бумажке и отдать кому-нибудь на вычитку будет гораздо быстрее.

Да, вручную. Несколько часов (больше двух), но у меня практики нет вообще. Вероятно при чуток большем опыте (больше привычки к досадным ошибкам и поведению системы при их наличии) минут 40 должно быть. Доказательства (с использованием тактик) практически нечитаемы, но писать их не так сложно.

Но кроме того, есть автоматизированые доказательтва. Попробую может вечерком.

На первом же тесте, который нарушит контракт, будет пример значения и точно известная ошибочная функция.

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

Кроме того, контракты, как я понял, это пусть довольно продвинутые, но всего лишь тесты. Т.е. ну на конкретном наборе данных у тебя отработало. А что с другим набором?

Ввероятно, лучшее что можно сделать, это рандомизированное тестирование, +-.

А доказательтво - это гарантия, что функция соответствует спецификации. Т.е. вот для любой такой ф-ции, оно будет работать как описано и всё тут.

Гм… Считаешь, что «если argmax от f xs равно какому то x, то существует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.» лучше понимается, чем «если argmax от f xs равно какому то x, то s = f x больше или равен любому элементу из map f x и x – первый элемент, для которого f x = s»?

Я говорю что при небольшой привычке проще читать мат. нотацию, чем код, Нотация более декларативна, что ли.

Впрочем, контракт можно и в терминах существует/для любого написать.

Да, теорему тоже можно написать тоже в терминах той функции другой функции. Не совсем пойму правда на вскидку что тогда нужно будет доказывать. Скорее всего корректность функции contract а потом её эквивалентность функции argmax.

Если резюмировать, то код контракта - это не совсем спецификация. Это в общем то довольно сложный код который надо запускать на разных данных чтобы найти ошибку. Т.е. это тесты. Пусть и улучшенные, но со всеми их недостатками.

Существуют истинные недоказываемые утверждения.

Ну и слава богу, потому что иначе программисты были бы не нужны (потому что система была бы разрешима).

Злобный матан, однако. Ты это всё вручную писал? У меня ощущение, что написать доказательство на бумажке и отдать кому-нибудь на вычитку будет гораздо быстрее.

Да, вручную. Несколько часов (больше двух), но у меня практики нет вообще. Вероятно при чуток большем опыте (больше привычки к досадным ошибкам и поведению системы при их наличии) минут 40 должно быть. Может даже 20. Доказательства (с использованием тактик) практически нечитаемы, но писать их не так сложно.

Но кроме того, есть автоматизированые доказательтва. Попробую может вечерком.

На первом же тесте, который нарушит контракт, будет пример значения и точно известная ошибочная функция.

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

Кроме того, контракты, как я понял, это пусть довольно продвинутые, но всего лишь тесты. Т.е. ну на конкретном наборе данных у тебя отработало. А что с другим набором?

Ввероятно, лучшее что можно сделать, это рандомизированное тестирование, +-.

А доказательтво - это гарантия, что функция соответствует спецификации. Т.е. вот для любой такой ф-ции, оно будет работать как описано и всё тут.

Гм… Считаешь, что «если argmax от f xs равно какому то x, то существует такой индекс ix, что x стоит на месте ix в массиве xs и для любого y стоящего на месте iy в массиве xs выполняется следующее: либо f y < f x либо ix <= iy.» лучше понимается, чем «если argmax от f xs равно какому то x, то s = f x больше или равен любому элементу из map f x и x – первый элемент, для которого f x = s»?

Я говорю что при небольшой привычке проще читать мат. нотацию, чем код, Нотация более декларативна, что ли.

Впрочем, контракт можно и в терминах существует/для любого написать.

Да, теорему тоже можно написать тоже в терминах той функции другой функции. Не совсем пойму правда на вскидку что тогда нужно будет доказывать. Скорее всего корректность функции contract а потом её эквивалентность функции argmax.

Если резюмировать, то код контракта - это не совсем спецификация. Это в общем то довольно сложный код который надо запускать на разных данных чтобы найти ошибку. Т.е. это тесты. Пусть и улучшенные, но со всеми их недостатками.

Существуют истинные недоказываемые утверждения.

Ну и слава богу, потому что иначе программисты были бы не нужны (потому что система была бы разрешима).