продолжая беседу

[juan_gandhi]

Т.к. есть такое европейское мнение, что рефакторинг - это метросексуальный аджальный метод продажи навоза юзерам, то я вдруг задумался - а что в Европе делают, когда их хакают и информацию воруют? Ну понятно, против воровства в Европе есть законы, например, GDPR; а в Швейцарии так даже масс шутинги запрещены (это мне швейцарцы когда-то сказали); но вот если случилось, так что тогда? Компьютеры сжигают на свалке, покупают новые, и пишут для них новые программы?

Ведь, я слышал, в Европе сначала на Z-notations и на Rational Rose весь дизайн правильно напишут, так что европейская программа не может быть неправильной, так что и рефакторить там нечего. Она совершенна.

И вот если она сломалась, то чо. Неужели с нуля переписывают?

Тесты-то понятное дело что не нужны; программист выполняет приказ менеджера, а менеджер не может ошибаться; и только плохой программист пишет код с ошибками. Немецкий код работает везде и без ошибок. Ой, тут сразу вспоминается Энигма, и три ушлых поляка, которые ее кракнули как раз перед Второй Мировой. 

Comments

[sassa_nf]

(I do get your jest, but can't help to expand on it)

No, not of correctness, but only that the corresponding theorem is proven.

Example:

Function a: List -> b: List sorts list a, if b_i <= b_(i+1) for all i.

Then functions

duh _ = []

duh2 xs = [head xs | _ <- xs]

clearly satisfy that theorem.

So one needs to start with the correct theorem involving a proposition that the output list is necessarily a permutation of the input list. How does one prove the "correctness" of the theorem?

[bamalip]

Проблема будет только с непроверяемостью самого ТЗ (с верхнеуровневой теоремой). Если же неправильно написаны промежуточные требования к модулям (более низкоуровневые леммы), то это сразу всплывет, поскольку из них невозможно будет вывести-собрать главную теорему.

[sassa_nf]

:) звичайно!

і проміжок між "треба відсортувати" (постановкою ТЗ) та записом у вигляді теореми.

[bamalip]

Ну конкретно цей приклад (сортування) ближчий до бібліотечної леми. Хоча проблема дійсно існує. Написали специфікацію на супутник, а він потім не туди полетів. Бо не туди написали.