n
мы говорим про доказательство корректности всего-лишь
Size: a a a
2019 June 10
n
оно не везде нужно, мягко говоря
MG
Оно не нужно только там, где потери от некорректности, помноженные на вероятность ошибки, меньше, чем стоимость доказательства.
n
с тем же успехом можно сказать, что тесты писать это тоже самое, что типы
n
Оно не нужно только там, где потери от некорректности, помноженные на вероятность ошибки, меньше, чем стоимость доказательства.
и таких мест в быту полно
MG
Но это неинтересные места, там денег мало :)
n
у меня много :)
n
и того и другого
VL
Рич и Стю Хелловей и другие матерые Кложуристы они конечно авторитетные, но иногда хочется чтобы они год-два в Хаскеле посидели. Так, для профилактики.
May be not вроде говорит, что посидели немного
AI
Та ладна. "Сара по телефону напела" а не "посидели"
VL
Посидели и maybenot
n
Та ладна. "Сара по телефону напела" а не "посидели"
а можешь развернуть, зачем им там сидеть?
n
основной поинт Рича еще со времен Simple Made Easy ровно в том, что надо не автоматически проверять корректность, а сделать процесс поиска косяков простым и очевидным занятием
они сначала это сделали, а потом сверху добили спеком
они сначала это сделали, а потом сверху добили спеком
AI
а можешь развернуть, зачем им там сидеть?
Не могу. а) я в электричке б) я аргументированно доводы приводить не умею, только пиздеть. Иначе чего бы я в этом чате сидел?
n
вот это щас обидно было!
MG
Спек, конечно, очень помогает, но он для, опять же, программиста, а не безопасника.
MG
Мне было бы очень интересно почитать секурити-аудит какой-нибудь большой программы на языке с динамической типизацией (идеально - Clojure+spec, но какой угодно сойдёт), которая выставлена в Интернет.
VL
Ну вроде бы кложа решает это выводом состояния в отдельное место, а чистые функции довольно хороши и в лишних типа не нуждаются, а где надо - spec, она ещё и в ран тайме и с данными работает а не с кодом
MG
Да ладно.
MG
Я же приводил пример: вот есть функция. Она возвращает неотрицательные числа, но если ей передать
nil, то она вернёт -1. Как трассировать в обе стороны: и что будет с системой, если вместо неотрицательного числа будет -1, и не будет ли где-нибудь ситуации, когда nil будет передан?