Pull to refresh

Comments 858

Я нахожу несколько забавным, что раньше в комментах автор высказывал своё «фе» в адрес типов в угоду тестам, но в статье о тестах уже предпочёл умолчать.

И да, типы на пригодных для использования языках — часть документации. Рассуждения о том, что она может устареть, — абсурдны. Код тоже может устареть, вообще-то, почему этого никто не боится?

А кто вам, собственно, сказал, что устаревания кода никто не боится? Вы вообще, например, в курсе, какой объем айтишной экономики ушел на то, чтоб слезть с флеша? Это всё потому, что никто не боится устаревания кода, ага.

Ну и касательно документации — это как с бекапами. Есть люди, которые еще не работали с устаревшей, неактуальной, или попросту плохой документацией, и есть люди, которые уже работали. Удивляться тому, что последние предпочитают при малейших сомнениях глянуть в код — как минимум странно. Код не врёт (особенно если вы его сами собрали), а установить, врёт ли документация — не представляется возможным без существенных расходов.
Я нахожу несколько забавным, что раньше в комментах автор высказывал своё «фе» в адрес типов в угоду тестам, но в статье о тестах уже предпочёл умолчать.

Диффамация, я такого в общем случае никогда не утверждал. А даже если бы и утверждал — почему я должен говорить о тестах в заметке, посвещенной типам? А если и должен — то вот же внезапно оно: «подробную документацию, с соответствующими doctest».


установить, врёт ли документация — не представляется возможным без существенных расходов

А зачем вообще добровольно использовать инструменты, которым вы не доверяете? Документация в тулчейне, которым я пользуюсь, — не врет. Никогда.

А зачем вообще добровольно использовать инструменты, которым вы не доверяете? Документация в тулчейне, которым я пользуюсь, — не врет. Никогда.

Зачем быть бедным и больным, если можно быть богатым и здоровым?

Ну и вы передёргиваете: если у меня есть возможность заглянуть в код — то я вполне могу доверять инструментам (код хороший) и при этом не доверять документации (документация плохая).

Я черным по белому написал: инструмент может быть признан хорошим тогда и только тогда, когда у него идеальная документация.

Да, когда вы по разным не относящимся к делу причинам миллиардер — то жильё может быть вами признано хорошим тогда, и только тогда, когда оно в 300 кв.м. и идёт в комплекте со штатом прислуги.

Я ж говорю, это аргумент из серии «ну вот смотрите, я здоровый и богатый, чё б вам всем такими не быть»?

Неправда. Мы обсуждаем код (и типы, и документацию) — написанную нами самими. Никаких проблем создавать документацию, тут не нужно быть миллиардером.

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

Действительно, никаких проблем: вот тебе многомегабайтный легаси-код, который по чисто экономическим причинам мы несколько лет поддерживали силами одного полупрофессионала, а теперь наверни нам на него модную обёртку. И, опять же, по чисто экономическим причинам, времени на то, чтоб написать/обновить документацию легаси у тебя не будет.

Действительно, и при чём тут экономика и миллиардеры?

ЗЫ: Всё вышенаписанное — это, к слову, не абстракция, а личный опыт.
вот тебе многомегабайтный легаси-код

Там и типов нет, наверное ведь. Давайте сравнивать сравнимое, пожалуйста.

На яве типы есть даже в дремучем легаси. А вот актуальной документации может и не быть, если несколько лет никто не занимался её поддержанием.

Это ваш собственный критерий, и не все могут себе позволить ему следовать.

>А зачем вообще добровольно использовать инструменты, которым вы не доверяете?
Хм. Вот у меня инструменты допустим Hadoop и Spark. Ну, там еще с десяток других наверное наберется, но это уже неважно. Вы думаете, у меня есть много альтернатив? Я бы сказал, что нет — ни одной вменяемой не наблюдается. И даже если бы они были, стоимость перехода на любую из них будет совершенно запредельна.
К разделу «Неверная ветка»: вообще для таких случаев есть методы вида valueOf.

Не понимаю, если честно, как valueOf поможет в случае, когда мы перепутали что вернуть (там в примере перепутаны, грубо говоря, if и unless).

UFO just landed and posted this here

Я 20 лет без малого пишу на perl, и мне не хватает типов. Как только мы выходим за пределы sum, начинается веселье. Я сейчас поддерживаю старое процедурное cgi легаси, и мне очень, очень непросто ловить ошибки.

UFO just landed and posted this here
вот чтобы проблема и "а были бы типы, проблема была бы решена"

Я вот, кстатит, легко приведу.


Было у меня два сервиса, делавших приблизительно одно и то же. На питоне. В какой-то момент мне понадобилось сделать так, чтобы они возвращали полностью идентичную структуру данных. Так вот, сделать это, сказав "вы возвращаете такой-то тип", оказалось намного проще, чем писать тесты на всю структуру. И изменения этой структуры тоже стали намного легче.

Так сделайте это для этой конкретной структуры, в чем проблема-то? Ну там, не знаю, класс с лоадером создайте.

Что "это" вы мне предлагаете сделать для конкретной структуры?

Возвращать «полностью идентичную структуру данных», пропуская сырые данные через валидатор.

пропуская сырые данные через валидатор.

… который надо написать, да? И чем это от тестов отличается?

>Если силы потраченные на сильную типизацию потратить на написание тестов, то результат будет лучше!
Не будет. Тесты вам почти ничего не гарантируют, в отличие от типов.

Да, языков с реально мощной (и одновременно удобной) системой типов пока немного, но то, что вы сможете описать на типах — будет как правило работать, если скомпилировалось.

Для тестов же это неверно в общем случае — если тест отработал, это может вообще ничего не значить.

Кроме того, то же самое, что обычно сложно описать на типах — так же сложно описать и в тестах. Условный немного пример — пусть вам нужна устойчивая сортировка. Попробуйте сформулировать тест, который проверит этот факт?

>программист делает АЛГОРИТМИЧЕСКУЮ ошибку и типы никак не помогают
Вы ждете от типов, что они вам исправят использование минуса вместо плюса, или речь о чем-то другом?
UFO just landed and posted this here
>тесты нам гарантируют что код выполняется будучи прогнан по набору тестовых входных вариантов.
Ну вообще-то это и называется «не гарантирует» ))) На этом работает — и больше возможно ни на чем. Или если быть точным — тесты не гарантируют отсутствия ошибок.

По поводу практически применимых языков — ну вот смотрите, у 0xd34df00d был пост с в общем-то простым примером — инвертированием списка. И код, реализованный без единого запуска, но зато с доказательством. Суть которого проста, как огурец — инвертированный список должен в качестве результата левой свертки давать то же значение, какое не инвертированный дает для свертки правой. Или наоборот, не суть.

Это не такой простой для доказательства факт, как его формулировка. Но если вы такое доказательство проделали — то тест из него делается одним пинком. Но при этом, доказательство, работающее в момент компиляции, все равно останется более полезным. Ну то есть, перенести проверки в рантайм мы как правило можем всегда. А цель строгих систем типов — как раз перенести проверки в компиляцию. Все какие сможем.

Автор, кстати, предлагает вполне разумные вещи. Guards там, или паттерн матчинг, тотальные проверки аргументов функций. И по сути, строгая типизация, как я ее вижу, это примерно те же самые идеи, только выраженные другими терминами. По сути, guard это и есть то, что хотелось бы уметь выразить в типах функции и ее аргументов — только записанный в явном виде в коде. Ну и примененный в рантайме, а не при компиляции.
UFO just landed and posted this here
задача простого http-сервера — решается рядовым Джуном.

Серьезно?

UFO just landed and posted this here

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

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
а проблемы находятся тестами.

… которые, конечно, любой джун умеет писать.

UFO just landed and posted this here

а джуну говоришь "у нас такая парадигма: сперва пишем типы, затем пишем код" и он ей следует.

UFO just landed and posted this here
с написанием на типах простого http эксперты не справились.

А вы можете доказать это утверждение как-то?

UFO just landed and posted this here

Нет там пруфа утверждению "эксперты не справились с написанием на типах простого http". Ни в части "эксперты", ни в части "простого".

UFO just landed and posted this here
проект-флагман
проект-"самый быстрый сервер!"

И именно это опровергает ваше утверждение про "простой http".

UFO just landed and posted this here

Проект "самый быстрый сервер" — это не "простой http". Простой http — это тот, который поддерживает протокол.

UFO just landed and posted this here
самый быстрый — это тот который использует самый быстрый механизм операционной системы работы с сокетами.

Во-первых, совершенно не обязательно.
Во-вторых, если с "самым быстрым механизмом" работать сложнее, чем с медленным, то это как раз и делает разработку сложнее.


первично что проект "самый быстрый" == "ничего нового в алгоритмах"

Совершенно не обязательно.

UFO just landed and posted this here
ибо скорость определяет именно он (самое узкое место в нём).

Если самое узкое место в нем, то он определяет скорость. Но ведь может быть и не в нем.

UFO just landed and posted this here
над этим вопросом работают много коллективов и в том числе разработчики OS.

Какое отношение "разработчики OS" имеют к тому, где у меня в коде узкое место?


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

UFO just landed and posted this here
и если Вы претендуете на звание "самый быстрый", то это значит на своей стороне сделали всё возможное чтобы скорость была максимальна.

… и вот ровно это и не является простой задачей, о чем и шла речь с самого начала.


всё равно идёт вызов системного метода.
который и будет самым медленным во всех реализациях http

Конечно, не во всех.

UFO just landed and posted this here
потому что ничего алгоритмически нового в ней сделать уже нельзя

Не-новое — не обязательно простое.

UFO just landed and posted this here

… и вы предлагаете вам просто поверить на слово в этом, так ведь?

UFO just landed and posted this here
любой джун реализует http сервер.

Да-да-да, вы уже это говорили. Этому вы тоже предлагаете верить на слово.


потом попрофилирует код

Знаете, в моем понимании джуны особо не умеют код профилировать.

UFO just landed and posted this here
Вы предлагаете верить на слово тому что джуны не умеют профилировать.

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


давайте теперь, докажите это Ваше утверждение

Утверждение о моем понимании чего бы то ни было доказывается очень просто: я — единственный авторитетный источник в этой области.


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

Вот типичный пример, да. В вашем понимании, похоже, джун обязательно учился в ВУЗе по какой-то программе, которую вы видели. А в моем понимании — и опыте — это не так.

UFO just landed and posted this here
почему я должен верить Вашему пониманию

Не должны. Но это показывает, что ваши и мои утверждения о джунах и работе для них нельзя трактовать одинаково.


средний джун учился в ВУЗе

… каком-то, наверное, да. Как-то учился.

джун или учился в ВУЗе или изучал это самостоятельно

средний джун учился в ВУЗе

Хм… Ну да, учился. Я вот учился на эконом факе с/х академии.
UFO just landed and posted this here

Ну так вы и не джун, я полагаю.

UFO just landed and posted this here

Да даже парсер http протокола не задача для джуна.
А сервер это абстракция над ним и определённо сложнее.


Или ваше "реализует" подразумевает "склеить существующие решения"?

UFO just landed and posted this here
UFO just landed and posted this here

А вот если я буду делать что-то более сложное, то, внезапно, узким местом может оказаться совсем не сокетная система.

с написанием на типах простого http эксперты не справились.

Я на хаскелле после прочтения learnyouahaskell, который по продолжительности и сложности меньше тур де го, смог написать на серванте простенький веб-сервер, который умеет пару объектов в JSON отдавать и в сваггер. Всё в типах описал, оно подняло всё, что мне нужно.


Каким экспертом нужно быть чтобы пройти вводный курс по языку и посмотреть на examples в репе?

а джуну говоришь "у нас такая парадигма: сперва пишем тест, затем пишем код" и он ей следует.

Следовать-то следует. В том смысле, что он пишет тесты до того, как пишет код. Но откуда взять уверенность, что он пишет правильные тесты?

Справедливости ради, уверенности, что джун пишет типы правильно, тоже нет. Как-то раз встретил код на typescript, где все ошибки типизации глушились через as SomeType

как-то раз встретил код на typescript, где все ошибки типизации глушились через as SomeType

На это достаточно легко настроить статический анализ.

Это тоже можно обойти, например, через любую функцию возращающую any (например, пара JSON.parse/JSON.stringify). Мой поинт в том, что аргумент ад джунум плохой, потому что любой инструмент можно использовать неправильно

любой инструмент можно использовать неправильно

Но неправильное использование некоторых инструментов проще заметить, чем других. Вот мне проще определить неправильные типы, чем некорректные юнит-тесты.

и пишет тест, который ничего не тестирует

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

Да, это лучший (я не иронизирую) аргумент против тестов, но именно поэтому некий Джон Хьюз придумал… ну, вы в курсе :)

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

Вовсе нет, просто пример утрированный. Тестами нельзя ничего доказать, типами (настоящими, не теми, которые, например, в Java, и даже не теми, которые сегодня есть в Хаскеле) — можно.


Отрицать это довольно странно. Просто есть широчайший спектр задач, которым формальное доказательство, добытое невероятной ценой (например, убеждением шефа в дееспособности Агды в продакшене), — не уперлось.

UFO just landed and posted this here
UFO just landed and posted this here

Я понимаю правильно, что вы решили таки проблему останова?
Пусть даже в "элементарном" случае HTTP сервера.

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

HTTP это текстовый протокол. Соответственно ответ сервера выглядит как строка начинающаяся как GET HTTP 1.1\r\n..., поэтому и сериализация в строку совершенно нормальна.

Если надо объяснять, то не надо объяснять.

UFO just landed and posted this here

Прямым.Имея строго типизированные вещи вы можете доказать конечность отдельных частей либо её отсутствие.
В слаботиптзированой каше — вы успокаиваете себя "зеленым кружочком" прошедших тестов и более ничем.

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

Ну парсер, по типам же видно. Пытается получить всё до \r\n или двоеточия, считаывает ключ (всё кроме двоеточия, за которым следуют опциональные пробелы), затем по той же схеме считывает значение (всё, кроме символа перевода строки). Потом упаковывает tolower ключ и значение, результата — тапл двух строк.


В случае ошибки видимо возвращается Left "ParserError" или что-то схожее.


Какие нормы "программизма" правда нарушает непонятно. Взяли спеку, посмотрели что там написано "чтение заголовков", прочитали заголовки.

UFO just landed and posted this here

Откуда я знаю какой файл? Я читаю то что вот тут кусочек скинут, и рассказываю что он делает, если у вас с восприятием ML проблемы. Я сам пару месяцев как начал изучать, но для того чтобы без проблем понимать базовый синтаксис этого хватает.


Парсит он, очевидно, входящий стрим символов. Потому что SRP, и парсер заголовков ничего не знает про то, прислал ему клиент данные или мы например в файл сохранили HTTP запрос и теперь его парсим (такой функционал, например, есть в фиддлере).

UFO just landed and posted this here
если это он же используется для парсинга Request, то я сразу уволил бы того кто это написал.

Почему? Что тут не так?

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
то наткнувшись на этот заголовок, можно сразу выбрасывать код в мусорку, а его писателя увольнять.

Почему вдруг?

UFO just landed and posted this here

Я в таких случаях склонен считать, что говорящий это просто не умеет объяснять.

UFO just landed and posted this here
так исторически сложилось что false обозначают нулём, а true обозначают не нулём.

Ну не знаю. По мне, "так исторически сложилось", что true и false обозначают разными вещами, а 0 там или 1 — мне более менее все равно.


Хотя, конечно, я не люблю, когда булевые понятия обозначают числами.

UFO just landed and posted this here

Это меня не удивляет, учитывая вашу нелюбовь к типам вообще.

UFO just landed and posted this here

Я, конечно, в этот момент должен бы почувствовать себя необразованным быдлом, но, к счастью, нет.

UFO just landed and posted this here

Я же не говорю, что это ваш интент, это скорее небольшая рефлексия.

UFO just landed and posted this here
что на простой задаче у них началась война safe'ры против unsafe'ров

Да что вы говорите. Простые вебсерверы на расте, написанные без всякого unsafe и очень sound кодом — существуют. Война началась как раз там, где, судя по всему (хотя я не вдавался в мелкие детали) ради выжимания последних процентов быстродействия (что даже в вашей системе координат простоты никакой «рядовой джун» не сделает) код стал таким себе.
>Их типы реальных задач и не решают.
Ну блин… типы не об этом. В остальном — ну где-то вы правы, в главном — что реально мощные типы пока далеки от практики на сегодня.
UFO just landed and posted this here
и когда вам говорят: не противопоставляйте типы и тесты, вы же не слышите
WAT?!!! Ведь именно автор и начал пытаться противопоставлять тесты типам и на основе этого пытаться доказать, что типы бесполезны!
UFO just landed and posted this here

Ткните пальчиком, где именно?


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


Спасибо.

Извиняюсь, настолько обчитался комментариями, что некоторые из них начал воспринимать как часть статьи.
UFO just landed and posted this here
Ну, где я-то противопоставлял? Я лишь все время подчеркиваю, что тесты имеют ограничения. По той простой причине, что это не способ доказать что-либо, а лишь проверить, что частный случай работает (и да, я тут тоже про типичные современные языки, где даже property based тестов обычно нифига не найдешь, а есть лишь обычные unit, с одним набором параметров).
UFO just landed and posted this here

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

UFO just landed and posted this here

Это не похоже на требования к программе. Советую за этим сходить в кафе или бар поблизости.

Ну я в общем скорее про целесообразность — т.е. если и могут — то практически пока неудобно.

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


Один из хороших примеров, когда я делал структуру


public class IdOf<T> { 
   public Guid Value {get; } 
}

с фантомным типом T. Все айдишки были гуидами поэтому можно было передавать вместо айди юзера айди заказа например. А с этой штукой такие проблемы стали ошибкой компиляции. Вот было у вас:


public User GetUserById(Guid userId) => 
  users.SingleOrDefault(x => x.UserId == userId)

и вызывали вы


GetUserById(user.OrderId)

Работает, но неправильно.


После фикса становится:


public User GetUserById(IdOf<User> userId) => 
  users.SingleOrDefault(x => x.UserId == userId.Value)

ну и соответственно


GetUserById(user.OrderId)

Падает с ошибкой "ожидался айди юзера, а передан айди заказа".


Вот так очень простой тип на 4 строчки решает довольно часто встречающуюся проблему "случано отдали не ту айдишку". Какие тесты тут бы помогли? Ну, наверное какие-то написать можно, но наверняка большинство скажет "тут нечего тестировать, нужно просто быть внимательнее".


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

Ну, я бы сказал, что уже приведенный ниже пример с алиасами из скалы делает что-то примерно похожее. Так что в итоге «неудобно» — это совсем массовые языки, и не очень новые. Java типичный пример — типы есть, но выразительные возможности — так себе.

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

Не всегда получается. Хотя я пытаюсь заменять Java на Scala, и мне на сегодня нравится результат.

Скала довольно неплоха, особенно с выходом дотти. Поковырял его — весьма неплохо. Хотя ML синтаксис мне всё больше нравится, но не думаю что кто-то сможет сделать с ним популярный язык. А жаль.

Эх, блин. дотти… нам до версии scala 2.12 как до луны пока… Хадуп живет на Java 1.8. Задачи по его переводу на Java 11 уже много лет открыты в JIRA.
А что, дотти (0.21.0-RC1) уже применима в реальной жизни? Я догадываюсь, что к спарку ее хрен прикрутишь, это его самого нужно будет пересобрать (что как минимум лениво), но хотя бы для изучения уже можно брать?

Для изучения можно. Стабильная версия должна выйти до конца года.

UFO just landed and posted this here

Вы юнит-тестами базу тестируете?

UFO just landed and posted this here

Вы в курсе о концепции mocks и прочем?
Чем вам помогут тесты на тестовой базе?
Как вы убеждаетесть, что на тестовой работает и будет на проде?

Оу, кажется сейчас будет повтор одной занимательной дискуссии, которую я имел ровно с этим оппонентом ровно по этому поводу.

UFO just landed and posted this here

Как вы доказываете, что ваш тест на тестовой базе тестирует продакшн сценарий?
Или снова будет "а у меня работает, значит правильно"?

UFO just landed and posted this here

Ну то есть ваши тесты ничего не дают кроме "у нас всё ок, в тестовом докере".
Где "консистентность" вашей тестовой базы и реального мира продакшна?

UFO just landed and posted this here

Это заявление об идентичности бд очень актуально, когда прод бд на 1ТБ. Как только Вы берете срез БД вместо целой БД — идентичность вылетает в трубу. М вместо одной вещи (тесты) приходится начинать думать о двух (+ правильный ли срез БД мы взяли). Я уж не говорю о том, что время выполнения теста на большой бд может быть неприлично большое.
В общем, типичное непонимание пирамиды тестов и юнит-тестов, в частности

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

Вообще типы — это как раз про задачи такого уровня.

> это те, которые сводятся к одной функции без каких либо зависимостей.
Ну то есть, я бы сказал, что вот такие.

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

Ну вот. По большому счету это все, что умеют типы в современном массовом строго типизированном языке. Ну то есть, если вы скажем про… Java, то вы скорее правы, чем нет. Правы — потому что система типов Java проблему написания джуном веб сервера не решает (хотя и помогает например рефакторить очень сильно). Но с другой стороны, система типов Java — она уже очень старая (ведет свою историю с версии 1.5, 2004 где-то), т.е. прошло уже 15 лет, и с другой — сразу с рождения была legacy, потому что сделана с целью получить совместимость с тем, что было до 1.5.

Ну то есть, современные нам массовые языки — они не так чтобы очень уж хороши в этом плане. Сами по себе — по сравнению с языками со слабой типизацией все как раз нормально. Те которые хороши — пока не массовые. Про Rust не скажу, так как просто не знаю.
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

Не обязательно. Например, при минимальной поддержке IDE после того как я нажму двоеточие у меня автоматически напишется return a + b, и мне останется только дописать код выше этого return'а.


А вот в тесте точно придется дублировать код, описывая expected.

Не совсем понятно при чем здесь сравнение ошибки компоновки функций и ошибка в логике функции?
UFO just landed and posted this here
UFO just landed and posted this here

Я предлагаю сойтись на том, что выразительная система типов страхует программиста от определенного (достаточно ощутимого) класса ошибок
Примеры, что будет, когда ее нет — уже были выше, например, передали uuid заказа, вместо uuid пользователя.

UFO just landed and posted this here
Вот только покрыть тестами то, что покрывается типами на порядок дороже.
UFO just landed and posted this here
Ну что ж. Я вижу из этого только один выход.

Всё что возможно — покрывается типами. И только то, что невозможно покрыть типами — покрывается тестами.
UFO just landed and posted this here
то есть 10% покрываем типами
90% тестами

Откуда цифры?


при этом на покрытие типами 10% проблем мы тратим примерно столько же сил как на покрытие тестами 40% проблем

Откуда цифры?


Собственно, у вас уже спрашивали, сколько тестов надо, чтобы покрыть то, что покрывает явная типизация fib.

UFO just landed and posted this here

Ну то есть эти цифры означают, что у вас (и, возможно, вашей команды), на используемых вами яхыках (каких, кстати?) получается покрыть типами в девять раз меньше, чем тестами, и в четыре раза меньше. Допустим.


Почему вы думаете, что у других (особенно когда у них другой тулчейн) так же?

UFO just landed and posted this here
потому что другие так же пишут программы живущие в реальном мире: ходящие по http, обращающиеся в БД итп

Ну да, я вот пишу. И у меня совершенно другие пропорции, нежели у вас.

90% чего вы покрываете тестами?


Ну то есть когда говорят, что 90% яблок зеленые, это значит что есть N яблок из 0.9*N штук из них имеют зеленый цвет.


Что вы взяли за N?

то есть 10% покрываем типами
90% тестами

50% типами за 10 у.е. усилий и 50% тестами за 50 у.е. усилий. Т.Е. типы в 5 раз более эффективные на единицу усилий.

Говорю с опыта поддержки кучи проектов на JS, TS и C#
при этом на покрытие типами 10% проблем мы тратим примерно столько же сил как на покрытие тестами 40% проблем

А сколько у вас строк тестов в среднем на 1000 строк кода? По типам оверхед обычно где-то ~5%

UFO just landed and posted this here
большую часть проблем выявляют тесты
Потому что тесты работают явно, а типы — нет. Тесты запустились, красные — пофиксил. Видишь их пользу.

И типы работают пока пишешь и пользы не видишь. Потому создаётся такая ложная иллюзия меньшего влияния.
UFO just landed and posted this here
UFO just landed and posted this here

(Мама, он первый начал!)


Какая разница, кто первый, если вы делаете утверждения от своего имени, вполне самостоятельные.

UFO just landed and posted this here
ну мы пришли в споре к тому что Вы согласились с моим базовым утверждением: тесты решают более обширный круг проблем нежели типы.

Не было такого. Более того, я вам неоднократно указывал на обратное.

UFO just landed and posted this here
я трактую это так что, B согласен с утверждением

Вот только утверждение "типы не решают вопросов нахождения алгоритмических ошибок. тесты — решают" не эквивалентно утверждению "тесты решают более обширный круг проблем нежели типы".


Поэтому даже если В согласился с утверждением "типы не решают вопросов нахождения алгоритмических ошибок", он не соглашался, как вы ему приписываете, с утверждением "тесты решают более обширный круг проблем нежели типы".


И уж тем более не надо приписывать реплики других ваших собеедников мне.

Поэтому даже если В согласился с утверждением «типы не решают вопросов нахождения алгоритмических ошибок», он не соглашался, как вы ему приписываете, с утверждением «тесты решают более обширный круг проблем нежели типы».
Не знаю, корректно ли так говорить, но они решают более обширный круг в определённом направлении.

Ну, с этой-то диаграммой и я согласен.

UFO just landed and posted this here
навскидку: типы не решают алгоритмических проблем.
тесты решают.

Навскидку: тесты не решают проблемы рефлексии по коду. Типы — решают.


когда программист печатает код, он конечно делает опечатки (то что решают типы)

Типы решают (далеко) не только опечатки.

UFO just landed and posted this here
навскидку — типы ухудшают рефлексию по коду

Так. Начнем с простого вопроса: что вы понимаете под рефлексией? Потому что я под ней понимаю возможность программно получить информацию об объектах/функциях.

навскидку — типы ухудшают рефлексию по коду
У вас странная, неполная типизация. Так какой тип вернётся? И вам кажется нормальным плюсовать комплексное число и флоат? Какой это язык вообще?
UFO just landed and posted this here
что значит неполная?

полная. на вход может прийти float, int или комплексное число

на выходе тоже будет оно же

Значит, что я не знаю, что будет на выходе. Ну, к
примеру что я получу на выходе?
sum(int, float)


Да я даже тут не знаю, что получу на выходе в вашем примере:
sum(int, int)


И это вы называете типизацией?
В любом случае такое (если очень нужно) можно было бы записать как-то так (псевдокод)

type Number = typing.Union[float, int, complex];

def sum(a: Number, b: Number) -> Number:
     return a + b


А вообще у вас этот код слишком динамический. Вместо того, чтобы сужать типы — вы их зачем-то расширяете. Это вообще довольно сомнительная типизация
UFO just landed and posted this here
то есть Вы предлагаете писать три функции сложения, отдельно для каждого типа?

Отдельно для каждого возвращаемого типа, если это нельзя вывести как обобщение.


а complex и int вместе сложить нельзя?

А результат будет какого типа?

UFO just landed and posted this here

Ну вот это и должно быть видно из сигнатуры.

UFO just landed and posted this here
То есть сложили голубцы с воробьями? В трёх голубцах три воробья, значит два голубца и два воробья — это где-то пять воробьёв, так?
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

… а теперь вы у результата пытаетесь взять мнимую часть.

UFO just landed and posted this here
текст над стрелочкой докажите

Кстати, о доказательствах. Вы покажете, как можно тестами гарантировать, что из функции всегда возвращается итератор?

UFO just landed and posted this here
тестами можно это гарантировать для покрытых тестами диапазонов.

А типами (в соответствующей системе) — для всех.


мы с вами (с маленькой буквы, чтоб не говорили что ники перепутал) выше выяснили, что 100% доказательств не бывает.

Нет, не выяснили.


теореме Райса, которая гласит: "100% кода нельзя доказать"

Теорема Райса гласит не это, но не суть.


Нам не надо доказывать 100% кода. Нам надо доказать конкретный код, и его, при определенных условиях, доказать можно.

UFO just landed and posted this here
нам надо получить уверенность за цифру близкую к 100% кода что мы написали.

Я не знаю, что нужно вам. А мне нужна конкретная проверка. Тесты ее могут или нет?

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

Утверждение "все задачи нельзя", прямо скажем, неоднозначно.

UFO just landed and posted this here

Ну об этом, собственно, и речь: нафига мне весь пул задач? У меня есть мои конкретные, и они доказуемы.

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

… обещаете перестать ссылаться на эту теорему?

UFO just landed and posted this here
lair не согласен, а я вот, допустим, согласен. Типы на практике не покрывают всех задач тестирования, которые могут покрыть автоматизированные тесты. А авто-тесты не покрывают всех задач, которые могут быть покрыты ручным тестированием.

Зато типы значительно дешевле тестов, покрывают самые главные задачи и дают дополнительные плюшки, которые не могут дать тесты — к примеру корректное автодополнение.

И только когда мы выжали всё из типов как более удобного инструмента — остаток покрывается авто-тестами.

И только то, что не покрыть за адекватную цену авто-тестами — проверяется руками.

На практике ещё на этапе типизации уходит под 70% ошибок, но она настолько дешёвая, легка и прозрачна в обращении, что этого просто не замечаешь.
lair не согласен, а я вот, допустим, согласен.

Тут главное — уточнить, с чем согласен или нет.

UFO just landed and posted this here
При чём тут вообще опечатка? Опечатки и в JS не будут работать — там будет ошибка.

Типы — это аналог "Проверки размерности" в математике. У тебя есть формула ускорения. Если размерность возвращается корректная «м/с2», значит формула с большой долей вероятности написана правильно.

А вот то, что где-то плюс заменён на минус — это уже опечатка. И да, такие мелочи покрывают тесты. Я ещё с школы помню, что проверка размерности (типов по сути) с наибольшей вероятностью находила ошибку.

И сейчас при адекватной типизации в итоге решение сводится к какому-то типу. Если свелось — значит оно корректно. И только опечатка может стать причиной ошибки. А вы сами утверждаете, что опечатки — это не так важно.
UFO just landed and posted this here
типы решают только проблемы опечаток в идентификаторах.

Нет.

UFO just landed and posted this here

Аргументы уже сильно больше одного раза были, и вы на них просто не ответили. Смысл их повторять?

UFO just landed and posted this here
UFO just landed and posted this here
основную проблему которую показывают типы

Нет.


когда str и int перепутались. но этой проблеме Ларри Уолл нашел решение четверть века назад

… и как же он предлагает решать проблему деления строки на число?

UFO just landed and posted this here

Эм. Ну то есть в каждом (публичном) месте, где мы ожидаем число, надо написать код, который приведет строку к числу (а вдруг нам передали строку вместо числа)? И бросить исключение? И обработать его уровнем выше?


Но зачем, если можно сказать "я принимаю только числа", и быть уверенными, что ничто, кроме числа, вы получить не можете?


Вот вам развлечение: приведите строку "123,45" к числу.

UFO just landed and posted this here
это делает сам язык.

А можете код показать?

UFO just landed and posted this here
$a = 'nope'

$c = $a + 1

М?

UFO just landed and posted this here
UFO just landed and posted this here

Ну вот давайте возьмем простую функцию, которая два числа складывает. Можете показать ее код?

UFO just landed and posted this here

И как сделать так, чтобы, если в $a не число, была ошибка?

UFO just landed and posted this here
включить варнинги — первый уровень (поматерится но посчитает)

Включить где?


но второй уровень в жизни обычно никому не нужен и никто так не делает

То есть мы получаем от внешнего пользователя "abc" и ^_^quotquot^_^, и возвращаем 1?

UFO just landed and posted this here
в коде, написав use warnings;

Внутри функции? Снаружи? Где угодно?


да и для реального мира это очень хорошее поведение.

Garbage In — Garbage Out — хорошее поведение? Я с вами не соглашусь. Если у меня некорректно формируются суммы в приходящих документах — это не хорошее поведение.


только у вас первоначально было 1 как одно из слагаемых

Привет парсеру.

UFO just landed and posted this here
там где нужно. распространяется на скоуп в котором применено.

А если применить в скоупе, который снаружи функции, на функцию распространяться будет?


итп

… так что с суммами в документах-то? Нормально, что они теряются? Хорошее поведение?

UFO just landed and posted this here
на весь модуль в котором примените :)

То есть одна функция может поменять поведение всего модуля?


Вы опять об опечатках?

О нет, я о внешних системах. Шлет вам внешняя система документы, а вы их парсите и складываете к себе в учетную систему. В каждом документе — два поля (сумма до налогов и налоги, суммы с налогами нет), вы к себе пишете сумму с налогами (складывая одно с другим). Внезапно вместо налогов начинает приходить строка Applied, в том самом поле.


Что получится с вашими правилами сверху?

UFO just landed and posted this here
Вы же применить его ВНЕ функции собрались?

Нет, я спрашивал о том, как определяется зона действия use warnings.


А, я понял. У вас не бывает функций внутри функций, да?

UFO just landed and posted this here

Я все-таки не понимаю, что будет, если написать use warnings внутри функции.

UFO just landed and posted this here
в этом месте лучше упасть по Вашему?

Ну да.


по моему лучше посчитать то что можно

А что тут можно посчитать?


проинформировать мониторинг о проблемах

Ну так если упасть — мониторинг автоматически проинформируется.


Более того, еще и сопряженная система проинформируется, что особенно хорошо.

UFO just landed and posted this here
пользователь получит 500

Неа. Пользователя там нет, там есть клиентская система. То, что она получит 500 (на самом деле — 400, но не суть) — это хорошо, потому что теперь все знают, что что-то пошло не так.


А пользователь не получит кривых данных. Что тоже хорошо.


всё что можно стоит посчитать

Там нет ничего, что можно посчитать. Было два числа, стало одно.


то такая ситуация (отсутствие валидации ввода)

О! Валидация данных! Это внезапно, потому что раньше речь шла о "для реального мира это очень хорошее поведение". А теперь, внезапно, мы что-то валидируем.


Значит ли это, что это не хорошее поведение?


остальное тестами покрыто

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


Проще говоря, сколько вариантов входных данных будет для теста функции?


def create_document_from(net, tax):
  return Document(total=net+tax)
UFO just landed and posted this here
тут выше были рассказы про сваггер — отлистайте.

Какой-такой сваггер? Нет никакого сваггера. Есть пропьетарный формат.


на самом деле до этой функции не дойдут такие данные

Вы же понимаете, что в этом случае у меня будет вопрос "сколько тестов на то место, благодаря которому данные не дойдут".

UFO just landed and posted this here

Ненене, давайте на конкретных примерах. Вот есть "алгоритм", который принимает от недоверенного источника данные. Для простоты, этот алгоритм — это сразу вон та функция, потому что нет никакой разницы, где мы в стеке находимся. Ну в конце концов, выставлена у вас эта функция как публичный API модуля, мало ли.


Так вот, сколько вариантов входных данных будет?

UFO just landed and posted this here
давайте на конкретных примерах.

Давайте. Я его привел выше, и меня интересует ответ на него. Любые попытки выбрать другой пример я приравниваю к "я не знаю, как тестировать такой код".


И да, забегая вперед: мне искренне все равно, к чему вы приравняете мое нежелание говорить про actix-web, потому что у меня нет ни информации, ни мнения по этому поводу.

UFO just landed and posted this here
UFO just landed and posted this here
где надо валидируем, а где не валидируем — это хорошее поведение

Ага, значит, все-таки, валидируем. И, судя по всему, валидируем не описанными выше встроенными средствами языка (потому что, цитирую, "никто так не делает").


самое крутое что код похож на человеческий язык.

Я не очень понимаю, что мешает "человеческим языком" типы указывать.

UFO just landed and posted this here

Ненене, давайте не забегать вперед, и ставить галочки.


Галочка первая: принцип "получили что угодно — сложили с чем угодно" — не хорошо в реальном мире (в общем случае).


Галочка вторая: для того, чтобы гарантировать выполнение первой галочки, вы предлагаете писать код (вопреки ранее сказанной фразе "это делает сам язык").


Так? Или нет?

UFO just landed and posted this here
код писать надо

Ага, прекрасно, по двум пунктам согласились.


Теперь следующий вопрос: как в языке, в котором "решена проблема перепутанных строк и чисел", выглядит проверка на то, что оба входящих параметра — числа?

UFO just landed and posted this here
man stdlib:atoi/itoa и всякие dtoa?

Не, не man. Код покажите.


алгоритм задания звучит так:

… какого задания?

Я не очень понимаю, что мешает «человеческим языком» типы указывать.
Это Пёрл то человеческий язык?

… а я вот удержался и промолчал.

UFO just landed and posted this here

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


Покажите тем же людям, вот эту строчку, пожалуйста. При том, что да, мне кажется, что я осилил.

Эх, хорошо, что Пёрл уже умер
UFO just landed and posted this here
когда опечатался в названии переменной, её тип получился undefined и он несочетаем с тем что ожидает функция или выражение
Я просто не понимаю, о чём вы говорите. Оно ведь просто не скомпилируется. С типами или без.

Если будете продолжать вести дискуссию в том же духе, то я просто буду отвечать, что тесты нужны, чтобы раз их запустить, понять их бессмысленность и никогда больше не запускать. Ну чтобы соответствовать вашему уровню
UFO just landed and posted this here
применение таких языков например в вебе — растёт из за непрофессионализма
Интересно, какой язык порекомендует наш якобы «проффесионал» вместо джаваскрипта в вебе?
языки, которые компилируют код нужны в современное время в очень, очень, очень узких нишах

Шта? А я и не знал, что пятнадцать лет работаю в очень-очень-очень узкой нише… LOB-приложений.

Извините, но Вы несёте чушь. Я реально не понимаю — какое это может нести удовольствие, учитывая, что оппонентов все равно не убедите в своей правоте (т.к. Ваши доводы ни о чем).

UFO just landed and posted this here

Вот вам еще один пример проблемы, которую решают типы.


//можно или нет?
foreach(var user in GetUsers())
{
  //можно или нет?
  user.Block();
}

Типы отвечают на эти вопросы прямо здесь и сейчас. Тесты — не отвечают (потому что GetUsers предоставлена библиотекой).

UFO just landed and posted this here

Конечно, нет.


object GetUsers()
{
  if (youHaveNoRights)
    return null; //это не опечатка
  else
    return new [] {"user1", "user2"}; //и это тоже
}
дальше Вы задали риторическое «и что?». его можно рассматривать как два варианта:


Есть третий вариант: вы сказали какие-то утверждение, но я ожидал от вас какого-то вывода. Если я напишу здесь: «куры летают», а вы в ответ спросите: «и что?» — вы тоже «проиграли в споре»?

дальше Вы
Обращайте внимание на ники, мы разные люди.
UFO just landed and posted this here
Для того класса задач, которые могут покрыть типы — тесты значительно худший инструмент. От того, что тесты могут покрыть какие-то другие задачи они не становятся лучше в тех задачах, в которых они хуже.
Примеры, что будет, когда ее нет — уже были выше, например, передали uuid заказа, вместо uuid пользователя.
Да, мы натыкались на то, что система типов от этого не страховала. После первого же бага разделили их на условные UserId и OrderId.
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
Уже на этом этапе вы упретесь в тот факт, что число возможных вариантов запроса практически бесконечно, потому что http далеко не простой. И покрыть их все тестами с большой вероятностью невозможно.
UFO just landed and posted this here

Пример можно увидеть, с доказанной корректностью хотя бы на уровне 2хх — 4хх?

UFO just landed and posted this here
UFO just landed and posted this here

Мы уже с вами(?) обсуждали юнит-тесты и проблемы с переполнением?
SSL тоже работает, даже корректно, что не отменяет проблем.

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

UFO just landed and posted this here
UFO just landed and posted this here
то, что вы сможете описать на типах — будет как правило работать, если скомпилировалось

Это та самая ничем не подкрепленная религиозная вера, против которой я, в основном, и выступаю.

Это та самая ничем не подкрепленная религиозная вера, против которой я, в основном, и выступаю.

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

И первое, и второе — далеко не идеальны. Но тезисы о том, что типы — это «серебрянная пуля» для абсолютно всего — я пока что слышал только от вас.
Насколько я понимаю, вы же не пишете на строго типизированных языках?

За деньги — нет. Но я профессионал (мню себя таковым), и не могу себе позволить игнорировать тренды. Я даже на джаваскрипте иногда пишу, что уж тут говорить.

А тогда откуда вывод, что это вера? Я вот пишу — и для меня эффект вполне заметен. Я готов поверить, что вам типы не дают эффекта, но тут же как всегда — «термодинамика — палка о двух началах» — может не дают, потому что не могут, а может — потому что вы готовить не умеете, или скажем задача не слишком простая на сегодня для типов? Готовить пока сложно, тут даже вопросов нет.

Условный практический пример — если у вас часть кода скажем SQL база, то понятно что внутри нее слабая типизация. И на границе с ней есть проблемы, потому что никто не сможет помешать DBA с той стороны сделать ALTER COLUMN, и поменять тип — и внезапно вместо числа прилетит строка.
то, что вы сможете описать на типах — будет как правило работать, если скомпилировалось

для меня эффект вполне заметен [..] или [..] или [..] или [..]

Вам не кажется, что «будет, как правило, работать» и «эффект заметен» с миллионом оговорок — это не совсем диффеоморфные утверждения? «Вера» я говорил про первое. Со вторым, так-то, в принципе, согласен.

Это было в разных комментариях поэтому про разные языки, если что. Эффект уже «вполне заметен» на уровня Java, где типы конечно имеются, но мощность системы типов все еще достаточно мала. В скале уже ближе к «скомпилировалось — работает».

Ну то есть — то что я в этой частной убогой системе типов могу описать с моим уровнем квалификации за разумное время — то уже и работает. И по сравнению с javascript эффект заметен еще как. Как-то так.
Полностью поддерживаю. Ранее писал на достаточно простом языке с динамической типизацией, 4 года с копейками. Перешел на котлин год назад — эффекту не нарадуюсь, работать с кодом стало гораздо проще. Что с чужим что свой писать и поддерживать.
Если силы потраченные на сильную типизацию потратить на написание тестов, то результат будет лучше!

У меня вот прямо на этом месте вашего комментария возникло сомнение, что вы хоть раз в жизни тратили существенные силы на какие-то нетривиальные типы.

Просто потому, что если б тратили — вы бы пример про это приводили, а не про функцию sum (про которую вам уже раньше в комментариях всё объясняли, и да, типы в этом случае не длинные и не сложные).
UFO just landed and posted this here
какую пользу тут принесло указание типов? никакой

Серьезно?


То есть тот факт, что вызывающий код, который попробует туда запихнуть строку, при разумном тулинге сразу получит подсветку ошибки — это не польза? Равно как и то, что сделав for v in fib(5), тому же тулингу известно, что vint, и можно делать соответствующие подсказки — это не польза?


Я вот сам пишу на питоне, и при прочих равных предпочту размеченный код неразмеченному — просто потому, что мне будет проще с ним взаимодействовать.


тесты и типы решают в общем одну и ту же проблему — верификация написанного кода

Типы решают не только эту проблему.

UFO just landed and posted this here

Каким образом вы можете написать тесты так, чтобы эффект для вызывающего кода был хотя бы таким же?


Ну то есть объясню: я пользователь функции fib, я ее из модуля импортировал. Мне не надо ее писать. Мне не надо ее править. Мне не надо гарантировать, что она правильно работает. Но мне хотелось бы, чтобы мне было удобно с ней работать. Как мне в этом помогут тесты?

UFO just landed and posted this here
или Вы типы не применяете в вызывающем коде?

Применяю, я даже пример выше написал, как именно. И именно здесь у меня вопрос: как мне тесты помогут их заменить?


для вызывающего кода тесты так же важны для вызываемого

Не понимаю этой фразы. Тесты на какой код? На вызывающий или на вызываемый?

UFO just landed and posted this here
тесты здесь заменяют типы здесь

Нет, не заменяют. Я еще раз говорю: мне от типов нужно, чтобы IDE мне правильные подсказки делала. Как вы этого добьетесь тестами?


а тесты могут.

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


типы — это решение более узкого спектра задач по валидации кода.

Не только. Впрочем, я уже это писал выше по треду, и вы это там проигнорировали.

UFO just landed and posted this here
у нас с Вами разные цели.

Ну да. Но вы же говорите, что тесты — более общеее решение, а это значит, что они (тесты) должны покрывать и ваши цели, и мои.


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

UFO just landed and posted this here
UFO just landed and posted this here

Ничего не делаю. А должен?

UFO just landed and posted this here

Я вам повторю второе предложение комментария, на который вы отвечаете: "а должен?"


Я где-то говорил, что моя IDE ловит эти ошибки?

UFO just landed and posted this here

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

проблему которую видят (надеюсь) все

Вы уверены, что все видят одну и ту же проблему?


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

Кстати на расте это можно выразить уже сегодня:


fn sum<M: Unsigned, N: Unsigned>(x: M, y: N) 
-> Box<UnsignedGreaterThan<M>> {
   ...
}

И написать a — b уже не выйдет, будет ошибка компиляции

UFO just landed and posted this here

Ну выразите то же самое в типах, как будто это сложно:


fn sum<M: Signed, N: Signed>(x: M, y: N) 
-> Box<If<Is<Positive, N>, UnsignedGreaterThan<M>, UnsignedLessThan<M>> {
   ...
}

Выразили в типах? Выразили.

UFO just landed and posted this here

Выше написано Signed, если вы вдруг не заметили.

UFO just landed and posted this here

Ну зависит опять же от свойств которые вы хотите выразить.


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


Покажите тесты — будет вам то же в типах. А эта игра в кошки мышки "а щас я придумаю такое что изначально не закладывал, чтобы тебя посрамить" я играть не намерен.

UFO just landed and posted this here
программист делает алгоритмическую ошибку.

Делает


единственный шанс выявить это в типах — написать эталонный алгоритм в коде типа.

Да нет, оно выявляется автоматически. При попытке полученным значением как-то воспользоваться. Например, если мы доказали что min (a, b) возвращает минимальный элемент пары, и мы его вызывали для длин двух массивов, то использовать его в качестве индекса этих массивов компилятор не разрешит — пожалуется что возможен выход за границы. И тогда разработчик пойдет и увидит, что в реализации min случайно перепутал больше и меньше. Ну и исправит, конечно.


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

Как правило зашкварно сложная документация к библиотекам на питоне и жс, а в типах обычно 2-3 ограничения. Которые, как бонус, всегда актуальны.

UFO just landed and posted this here
код этого "автомата" который "автоматически" кто пишет?

Ну компилятор пишут разработики компилятора, очевидно.


у питона кастрированная система документирования кода, у жс её вообще нет

А где хорошая система?

UFO just landed and posted this here
что и тип описывает компилятор?

тип — это требование к коду, которое вам нужно. Очевидно, это информация, получаемая от клиетов, а не от компилятора.


А по типам генерировать код компьютеры уже давно умеют, с разморозкой.

UFO just landed and posted this here

Ну вот например у нас челик задал вопрос, почему такая композиция работает


f1 :: a -> Maybe b
f1 = undefined

f2 :: b -> Maybe c
f2 = undefined

f3 :: c -> Maybe d
f3 = undefined

fn :: d -> Maybe z
fn = undefined

comp'' = f1 >>> f2 >>> f3 >>> fn

А оказалось, что компилятор вывел что функции населены исключительно const None.


Ну и тот же id например компилятор может из сигнатуры вывести. Я понимаю, что это простые примеры, но на них-то всё работает)

UFO just landed and posted this here
UFO just landed and posted this here
выход за пределы границы массива — примитивная задача.

Да?


Как подтвердить тестами, что следующий код никогда не выходит за границу массива:


Foo(Bar b) => return _bazs[b.BazIndex];
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

И вы утверждаете, что если эти тесты написаны и проходят, невозможна ситуация, когда мы вызвали эту функцию, и получили ошибку "индекс за границами массива"?

UFO just landed and posted this here
как это невозможна, если мы это поведение тестируем?

Напомню задачу: надо доказать, что код никогда не выходит за границу массива.

UFO just landed and posted this here
UFO just landed and posted this here
остаётся варьировать вероятностями "вероятность того что не выйдет за границу большая, или маленькая"

Окей, как (с помощью тестов) доказать, что вероятность выхода за границу не превышает 0.001?

UFO just landed and posted this here

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

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

Вам уже приводили примеры тестов на операции с переполнением, вы успешно с них слились.
О каких учебниках вы говорите.
Сформулирую проще — кто докажет корректность тестов ваших?
В теории типов для этого есть мат. аппарат, у вас — только самоуверенность.
Опровергайте.

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
из рантайма проверку удалять мы не имеем права

Имеем, конечно, если можно на этапе компиляции доказать, что она избыточна. Что, кстати, компилятор C# и делает регулярно (как раз с проверками границ массивов).

UFO just landed and posted this here

Вы? Возможно. А я стараюсь следить за тем, что я спрашиваю, и на что отвечаю.

UFO just landed and posted this here
выше есть мой код "как раз с проверками границ массивов"

Вот этот код?


def get_value(array, index):
  if index >= len(array):
    return
  if index < -len(array):
    return
  return array[index]

Вы хотели другого переполнения, как выяснилось integer

Вы меня с кем-то путаете. Переполнение чисел меня не интересует.


А к приведенному вами коду у меня есть очень простой вопрос: как с помощью тестов доказать, что он никогда не выдаст ошибку "обращение по некорректному индексу"?

UFO just landed and posted this here
а как с помощью типов это доказать?

Не ко мне вопрос.

UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here
Если вы можете в компилтайме это доказать, то в рантайме у вас будет нулевой оверхед [...]

В воздухе явственно запахло макросами.

UFO just landed and posted this here
Если вы можете в компилтайме [...], то в рантайме [...], и компилятор вырежет нафиг все эти проверки

Ну вот же :)

UFO just landed and posted this here

Мат. аппарат уже доказал.
Мы не про переполнение массива, а про переполнение в целых числах, которое нужно проверить правильным тестом. И вы таки слились в предыдущем обсуждении именно на моменте "а кто докажет полноту и корректность тестов" даже на банальном сложении чисел, что в строго типизированном варианте не прошло бы даже компиляцию.

UFO just landed and posted this here
Теория типов.
Утверждаете, что она не работает? Ждем опровержения, а пока у вас тесты даже целочисленное переполнение не могут словить и приходится в рантайме null'ами баловаться.
UFO just landed and posted this here
UFO just landed and posted this here
UFO just landed and posted this here

Теорема Райса говорит, что существуют программы, для которых нельзя доказать интересующее вас свойство. Например, если мы попытаемся доказать что программа на питоне никогда не кидается TypeError, то:
Для каких-то программ мы сможем это сделать.
Но найдутся такие, для которых доказать это мы не сможем.

UFO just landed and posted this here
UFO just landed and posted this here
Например, наличие счётного числа тривиальных алгоритмов (по одному на программу, где каждый алгоритм тупо проверяет номер исходный текст на соответствие), проверяющих данное свойство для каждой из всех возможных программ, не противоречит теореме Райса

Не, ну тут надо осторожнее. Если обладание данной программой данным свойством невыводимо — вы какой "тривиальный алгоритм" подберете?

теорема Райса говорит что любой (== весь) код доказать нельзя
Нет. Вы неправильно поняли. Не весь код. Существует код, который доказать нельзя, а значит не весь код можно доказать. Но есть множество кода, которое можно доказать
UFO just landed and posted this here
UFO just landed and posted this here
НЕ ВЕСЬ == НЕ ЛЮБОЙ == ЛЮБОЙ НЕЛЬЗЯ
Не все машины чёрные == не любая машина чёрная == любая машина не чёрная

У вас прекрасная логика!
UFO just landed and posted this here
нет не слился, вот вам код, проверяющий переполнение

По-моему, это не переполнение, а выход за границы массива. Нет?

UFO just landed and posted this here

Почитайте, что такое переполнение (integer overflow)

UFO just landed and posted this here
Сложение его переполняет, например. Или умножение.
Но вы без теста словить его не сможете, а с тестом тоже не факт, что получится.

Я не очень понимаю, к чему тут этот код, и о чем вы говорите.

UFO just landed and posted this here

А я и не хотел от вас никакого переполнения. Меня интересовало (где-то выше, если я не ошибаюсь), как вы в тестах проверите обработку границ массива (потому что вы сказали, что это легко), и, что характерно, ответа я так и не получил.

UFO just landed and posted this here
я уже отвечал — так же как и вы в типах

Вы меня, опять же, с кем-то путаете. Я не говорил, что я знаю, как делать проверки границ массива "в типах".


Меня просто интересует ваше утверждение, что проверка границ массива — это легко.

У вас нет проверки переполнения «в типах». У вас проверка в рантайме/линтером.
UFO just landed and posted this here

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

… или вот, скажем, есть у нас api.


GET /file/{file_id}

file_id — GUID. Пишем соответствующий обработчик:


public Task<File> Get(Guid fileId)
{
   //...
}

И знаете, что удивительно? При попытке сделать GET /file/0 будет 404. И при попытке сделать GET /file/myfile.jpg — тоже.


Мы не написали ни строчки кода, который это проверяет. Мы не написали ни одного теста, который проверяет, как Get себя поведет, если в него передать не-GUID. Казалось бы, это ли не польза? А если добавить к этому, что из этого же описания обработчика автоматически сгенерился Swagger, который всем потенциальнм клиентам рассказал, что сюда надо передавать именно GUID (и что именно будет в ответе, потому что там File), количество пользы продолжает увеличиваться.


Что веселее, если мы поменяем нижележащий слой так, что он начнет принимать не GUID, а что-то другое, статический анализ скажет нам — здесь больше не работает, поменяйте тип выше. И это — поменять тип — приведет к тому, что все прочее поведение поменяется (будет другая проверка в роутинге, и другое описание в Swagger).


Но это, конечно, очень легко воспроизвести тестами.

UFO just landed and posted this here

… и как вам в этом помогают тесты?


(это не говоря о том, что Swagger, в каком-то смысле, это типы)

UFO just landed and posted this here

"Типы — это просто средство, которое..."


Тесты он не отменяет

Да понятное дело. Я-то спрашивал ровно обратное: как с помощью тестов добиться того, что мне в моем примере дают типы.

UFO just landed and posted this here
дык вам не типы это дают, а валидационный код

Вот только этот валидационный код без типов не работает.


который сгенерирован или рантайм работает по сваггер схеме.

У меня ровно наоборот, сваггер-схема генерится из типов.


этот код одинаков и у Вас и у меня

… у вас этот код — тесты?

UFO just landed and posted this here
результат у нас с Вами одинаковый.

Конечно, нет.


Но давайте сначала определимся, ваш (не важно, одинаковый, или нет) результат — он тестами достигнут?


а качество у меня выше

А это — не доказано.

А рефакторинг там же — тоже не пример? Тот, который в результате наличия типов всегда правильно работает?
UFO just landed and posted this here
если бы рефакторинг был бы не нужен, тесты бы тоже были не нужны.

Вы это сейчас серьезно?

UFO just landed and posted this here
если проект не планируется рефакторить (читай развивать), то после релиза и исправления пула ошибок — зачем ему тесты?

Ну так багфикс же.

UFO just landed and posted this here

Нет, конечно. Багфикс (обычно) меняет наблюдаемое поведение, а это противоречит определению рефакторинга:


Refactoring is the process of changing a software system in a way that does not alter the external behavior of the code yet improves its internal structure.

Есть проекты, которые не рефакторят и развивают.

>именно из за рефакторинга вся эта эпопея с тестами и затевается

Дело в том, что в типизированном языке (Java тут вполне достаточно, кстати), рефакторинг можно зачастую провести полностью автоматически. И код при этом не ломается. И тесты на этот случай вообще не нужны. Так что это ваше утверждение — оно как минимум слишком общее.
UFO just landed and posted this here