Степпер для SBCL - помогайте

Лопата и экскаватор, а так же палка-копалка тоже совершенно разные инструменты

Да. Но лисп и хаскель - одинаковые, т.к. трудозатраты при использовании +- одинаковые.

Безработный. Вот скоро дотрачу заработанное в Кроссовере и пойду искать работу снова.

Внутри SBCL? Тогда ты мегакрут!

Пока что я пытаюсь заманить тебя анонсами, которые не знаю, как выполнять :)

Ошибки в рантайме и в компилтайме отличаются по трудозатратам. На сколько я себе представляю можно выделить следующие факторы

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

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

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

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

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

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

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

Кроме того, приведу ещё один аргумент. Хотя порог вхождения и кажетсяс выше, но таки я бы отделил «реальный порог», от «яужепрограммист-порога». Думается мне что чтобы хорошо программировать на лиспе надо потратить не меньше усилий чем чтобы хорошо програмировать на хаскеле. По крайней мере судя по яваскрипту (против того же хаскеля). Поэтому я думаю лисповский/яваскриптовый порог не есть «настоящий» порог.

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

Коммутативный эффект, по личным ощущениям, очень большой.

Резюмируя, согласиться с утверждением не могу :)

Все эти пестики-тычинки-лопатки-экскаваоторы — это всё хорошо, понятно и замечательно. К сожалению, нераскрытым остался вопрос, а почему хаскель/агда/идрис должны заменить собой именно лисп, а не ruby/java/1c/C++, например?

gambas?

Другое дело, что есть родной виндовый VBS

Могу только удивиться в ответ: почему не ruby/java/1c/c++? Я такого не говорил. ну у с++, на первый взгляд, есть фича - управление памятью. Но я честно говоря после вот этого, не уверен что это действительно фича. Да и линейные типы подъехали уже. Тоже очень интересная вещь в смысле управления ресурсами, по моему.

Т.е. ваш тезис — haskell как вершина ЯП должен заменить собой все остальные языки! Я правильно понял?

гм, agda/idris :), Ну и на данном этапе, да. Ну и условно в той же степени в которой java/c# заменили все остальные языки. Потом ещё что то придумется. Но agda/idris ещё не промышленные. У хаскеля компилятор, либы, рантайм, stack. А у агды/идрис (пока) только фичи.

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

Тут конечно вопрос эк. эффективности - победят ли миллионы дешевейших индусов и украинцев или же технологии всё таки окажутся сильнее?

Пока в истории всё таки технологии двигались вперёд за счёт значительного повышения производительности труда.

минусами «сильных» систем типов можно считать высокий порог вхождения

Какие мы умные, прям тащимся от своей исключительности. Интересно, а как «высокий порог вхождения» сочетается с утверждением «развитые системы типов должны значительно выигрывать и при написании и в поддержке»? Так сложнее, или проще языки со статическими типами?

Ошибки в рантайме и в компилтайме отличаются по трудозатратам

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

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

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

Коммутативный эффект, по личным ощущениям, очень большой

Хорошо хоть не коммуникативный.

Коммутативный эффект, по личным ощущениям, очень большой.

Какое странное слово влезло... Читать как «суммарный эффект, по личным ощущениям, очень большой».

Какое странное слово влезло

Не, я понял, что ты хотел сказать «кумулятивный». Но получилось еще лучше - по твоему мнению «от перестановки слагаемых сумма не меняется». Фрейд расплакался от умиления....

Интересно, а как «высокий порог вхождения» сочетается с утверждением «развитые системы типов должны значительно выигрывать и при написании и в поддержке»?

Так же как экскаватор выигрывает у лопаты. Ну и что что учиться надо на эксаваторщика полтора года в ПТУ да ещё и опыт нужен чтобы хорошо владеть техникой. Один чёрт лопата рядом не стоит.

Так сложнее, или проще языки со статическими типами?

Сложнее или проще экскаватор чем лопата?

Сложнее конечно, ну и что?

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

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

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

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

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

Коммутативный эффект, по личным ощущениям, очень большой

Хорошо хоть не коммуникативный.

Сильный агрумент.

гм, agda/idris :), Ну и на данном этапе, да.

Вы не находите своё мнение несколько фантазёрским?

Ну и условно в той же степени в которой java/c# заменили все остальные языки.

Про до-диез не скажу, в глаза его не видел, но если у java и есть преимущества, то это ни разу не языковые фичи. Язык-то убогий весьма и многословный. Как вы объясните факт доминирования убогого недоязычка с вашей точки зрения?

Как вы объясните факт доминирования убогого недоязычка с вашей точки зрения

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

А вы как объясняете, любопытно?

продолжения

О, как раз эту штуку осиливаю, читаю всё подряд, что нахожу.

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

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

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

Сильный агрумент

Значительно сильнее, чем путать слова после пафосной речи.

Нет, я не утверждаю что это хороший подход (100% покрытие), но за последние годы я мигрировал от куда то из области «тесты нужны, но иногда» в область «100% покрытие - лучший из всех плохих вариантов»

Не очень понял смысл сказанного. Тесты нужны, или не нужны? ИМХО тесты, как и статические типы - это вариация на тему «доказательства правильности» программы. В таком контексте статические типы - это не вполне адекватное решение, т.к. проверяют только формальное соответствие аргументов/результатов, но не логическую корректность работы функции/модуля.

проекты на clojure

Так лиспятники же скопом и воем воют, что кложа — нелисп. Ну и хорошо, т.к. она получше лиспа, всю малину бьёт только jvm под капотом, хотя за её то батареек счёт у кложи и пошёл взлёт.

система типов (достаточно простая, но довольно эффективная) + автоматическое управление памятью.

Но ведь у ML/SML/Ocaml с этим гораздо лучше.

А вы как объясняете, любопытно?

Я нахожу, что богатство выразительных возможностей языка само по себе обладает решающим значением в академической сфере (пилить гранты на исследование свойств языков) и в юношеском сраче (у твоего $яп1 нет дженериков, а у моего $яп2 есть, следовательно моя пиписька длиннее твоей пиписьки аха-ха-ха-ха!).

В промышленности решают:

• экосистема
• сообщество
• корпорация, которая продвигает технологию, пока она ещё маленькая

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

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

Этот эффект не зависит от системы типов. Он есть всегда. Как и

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

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

Значительно сильнее, чем путать слова после пафосной речи.

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

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

Не очень понял смысл сказанного. Тесты нужны, или не нужны? ИМХО тесты, как и статические типы - это вариация на тему «доказательства правильности» программы. В таком контексте статические типы - это не вполне адекватное решение, т.к. проверяют только формальное соответствие аргументов/результатов, но не логическую корректность работы функции/модуля.

Моё мнение - на хоть сколь нибудь значимом временном промежутке (начиная, условно, с 2 лет) тесты нужны, причём 100% покрытие. Раньше я был другого мнения.

Однако, я думаю, что то что проверяется типами - не нужно проверять тестами. Как ты заметил это во многом тоже самое. «Сильные» системы типов значительно сокращают необходимость тестового кода.

По поводу логики - тут уж ничего не сделаешь, с логикой простых решений нет. Но далеко не все ошибкина «логику». Я бы даже сказал их «подавляющее меньшенство». Ибо если ты понял задачу, то как можно сделать ошибку в логике? Это уже менеджера ошибка а не программиста, скорее. Ибо надо удостоверитья что люди делают то что нужно. В основном то ошибки как раз таки «на типы». Т.е. пришло одно, ожидаем почему то другое. Не нашёлся класс вдруг (php, яваскрипт, ошибка в имени). Выход за диапазон. И прочее.

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

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

P.S. обязательная цитата из классика: «Тестирование может доказать наличие ошибок, но не может доказать их отсутствия». А успешная трансляция строго типизированной программы как раз доказывает отсутствие класса ошибок (или даже классов, если система типов достаточно навороченная).

Так лиспятники же скопом и воем воют, что кложа — нелисп

Это внутренние тёрки-разборки на тему «раньше было лучше». Кложа - это современный лисп. Может быть нынешний CL потомки, пишущие на кложе, будут рассматривать, как мы сегодня смотрим на какой-нибудь mac-lisp.

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

o.O o.O o.O!!!!!

Но ведь это неправда!!!!

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

В промышленности решают:

экосистема
сообщество
корпорация, которая продвигает технологию, пока она ещё маленькая

По моему идеализм. Решает бабло в промышленности. И статистически известно что на яве и сишарпе писать дешевле то что на них пишут. Почему на них писать дешевле - это как раз фичи языка (включая стоимость подготовки программиста), тут никуда не денешься. Включая дженерики и прочее.

То что существуют всякие лиспворкс , на мой взгляд, есть доказательство того что должны существать и другие оптимумы. И вероятно они сильно более «оптимальны» чем явовский, но порог подготовки программиста сильно выше, поэтому они не массовые. И я полагаю что оптимум который есть у идриса/агды/хаскеля может стать массовым. Т.к. хотя и подготовка программистов дороже, но системы типов позволяют сильно сократить кол-во багов. Думаю, это может быть массовым оптимумом из за того что профессионализм «отслеживается компилятором», в отличие от лиспов.

вот «мы поняли задачу так-то и сделали такие-то предположения, а оказалось всё совсем по другому» и составляют 90% всех страданий.

90% процентов страдания кого - админов? Точно не программистов. И в любом случае, никакой ЯП от таких страданий не поможет.

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

отнюдь. у вас менджмент по моему не шибко хороший.

наверное 90% всех страданий от того что заказчик «понял что хотел не так а чуток по другому». И вот в этих случаях системы вроде пхп и яваскрипта просто супербыстро загинаются под тяжестью народжающихся багов, потому как в более-менее большом проекте объективно невозможно всё помнить, а компилятор ничего ен проверяет. и получается - в одном месте починили, в 10 сломали, но никто не заметил, кроме, ясное дело заказчика, который зол как чёрт.

Упрости один модуль - усложнится другой

Нет. Сложность каждого модуля остаётся фиксированной.

увеличится количество модулей

Да.

Увеличение количества тестов съест их упрощение

Нет. С 2 простыми сущностями работать проще, чем с 1 сложной.

Есть мнение, что при увеличении количества простых сущностей сложность системы растёт линейно, а при увеличении сложности сущностей и их фиксированном количестве сложность системы растёт нелинейно. За доказательствами отправляю к Дийкстре и другим апологетам структурного программирования.

обязательная цитата из классика

В контексте обсуждения необязательная и неуместная.

По моему идеализм.

Вот и поговорили. ;-)

Почему на них писать дешевле - это как раз фичи языка

1. По фичам java'у только бэйсик с 1с не бьёт.

2. Если бы вдруг Дед Мороз перепил на Рождество и вдруг сделал так, чтобы для, допустим, перла появилось столько же знающего народу, библиотек и ide (а для жавы исчезли), то внезапно писать на перле было бы дешевле, чем на оной жаве. При этом все фичи языков остались бы без изменений.

И вероятно они сильно более «оптимальны» чем явовский, но порог подготовки программиста сильно выше, поэтому они не массовые.

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

Да,и только пошагового отладчика в нём нету. А ну давайте помогайте мне его писать.

По фичам java'у только бэйсик с 1с не бьёт

Да. Но вопрос в производительности труда, поймите. Никто не обещал что если у вас язык наполнен синтаксическим сахаром, то производительность будет выше. И сахарок - не совсем фичи, кстати.

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

Зарплата у Джона из лондона 9 тыс в месяц, а у Дебашиша из индии 4. Но так уж получается что Джоны на хаскеле пишут проект за 90 тыс, а Дебашиши на яве за 120. А индусы на php берут свои 65 тыс и сдают проект. Но только пользоваться им не получается.

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

Это не говорит о том что уменьшится количество тестов на строку кода, по моему

А ты ещё подумай на эту тему. Что проще протестировать, 10 различных «крутилок», которые однозначно регулируют каждая свой параметр, или 1 «крутилку» которая имеет несколько степеней свободы и взаимозависимо регулирует 10 параметров.

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

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

«Сильные» системы типов значительно сокращают необходимость тестового кода.

Они полезны когда нет тестов - это да.

Ибо если ты понял задачу, то как можно сделать ошибку в логике?

А если ты знаешь, что функция принимает int, как можно передать туда double? Ошибки в логике встречаются гораздо чаще, просто потому что программист неверно реализовал алгоритм. Даже если он на 100% понял задачу. Я, например, часто пишу на динамических языках в т.ч. работаю с чужим кодом и даже не помню когда последний раз возникала ошибка типизации, а вот ошибки в логике (некорректные реализации) просто каждый день.

А ты ещё подумай на эту тему. Что проще протестировать, 10 различных «крутилок», которые однозначно регулируют каждая свой параметр, или 1 «крутилку» которая имеет несколько степеней свободы и взаимозависимо регулирует 10 параметров.

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

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

А если без эмоций, что такое «собственная дурь»?

Увеличение количества тестов съест их упрощение

Нет. С 2 простыми сущностями работать проще, чем с 1 сложной.

Повторюсь: ты не можешь избавиться от сложности, свойственной задаче.

Есть мнение, что при увеличении количества простых сущностей сложность системы растёт линейно, а при увеличении сложности сущностей и их фиксированном количестве сложность системы растёт нелинейно.

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

обязательная цитата из классика

В контексте обсуждения необязательная и неуместная.

Она всегда уместна там, где начинается «а мы всё протестируем».

отнюдь. у вас менджмент по моему не шибко хороший.

А он везде такой. Это пытаются поправить с помощью всяких скрамов-канбанов, МВП и прочего, но пока не очень выходит.

а компилятор ничего ен проверяет

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

Гм. «ну и задачи ты ставишь, барин».

Ну условно тебе надо иметь десять степеней свободы. надо проверять десять входящих параметров и их сочетания.

От того что ты «разбил на модули» решать задачу легче не стало. Вот от того что ты «недоразбил на модули» стало сложнее.

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

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

Ещё раз , то что можно писать код лучше - не аргумент. Просто потому что с лучшим языком можно писать код «ещё лучше». Жаль что ты этого не понимаешь

ты не можешь избавиться от сложности, свойственной задаче

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

где начинается «а мы всё протестируем».

А где это начинается? Обсуждение про другое. Или у тебя триггер на слово «тесты»?

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

ну и зачем ты тогда решал сложную? я ж говорю тебе ты только от собственной дури можешь избавиться. иначе бы в мире не было вообще ничего сложного.

А где это начинается? Обсуждение про другое. Или у тебя триггер на слово «тесты»?

а я вот как то в том же контексте тебя понял. для справки.

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

Но если фичи не поднимают производительность труда, то зачем они вообще?

Джоны на хаскеле пишут проект за 90 тыс, а Дебашиши на яве за 120.

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

ну и зачем ты тогда решал сложную?

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

Но если фичи не поднимают производительность труда, то зачем они вообще?

Где гарантия что каждая фича поднимает производительность труда в сколь нубудь более-менее полном представлении?

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

Но программиста на жаве или php можно найти с высокой вероятностью, просто кинув яблоко в толпу, а программиста на агде или идрисе будешь пол года искать.

Ну я в курсе, это называется стоимость (подготовки) специалиста. потому что специалисту по агде надо предложить 12 тысяч, а не 9 как хаскелисту и не 4,5 как явисту и не 2.25 как пхп-шинку.

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

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

У хаскеля/агды/идрис в этом смысле, я надеюсь, есть огромное преимущество: можно учиться без преподавателя и квалификацию легко оценить. Это важно для массовой подготовки специалистов.
Если окажется что система типов действительно того стоит, то кадры будет значительно проще подготовит чем для того же лиспа (хотя это тоже фича системы типов, но это как бы её обратная сторона выходит).

Моё мнение, конечно.

ты не можешь избавиться от сложности, свойственной задаче

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

На это уже ответили.

где начинается «а мы всё протестируем».

А где это начинается?

Вот здесь: Степпер для SBCL - помогайте (комментарий)

Или у тебя триггер на слово «тесты»?

У меня триггер на «мы лучше будем тестировать, чем проверять типы статически».

Не знаю, это же ты утверждал, что тесты - это сложно

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

я утверждаю, что тесты «если избавиться от дури» - это не сложно.

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

И что статические типы менее универсальный способ проконтролировать правильность программы по сравнению с тестами.

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

У меня триггер на «мы лучше будем тестировать, чем проверять типы статически».

А, ты про это

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

Доказывает только синтаксическую правильность программы. От этого как бы ни жарко ни холодно. Корректность использования проверяется только тестами.

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

Доказывает только синтаксическую правильность программы.

фейспалм

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

Доказывает только синтаксическую правильность программы. От этого как бы ни жарко ни холодно. Корректность использования проверяется только тестами.

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

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

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

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

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

Да я вообще не понял, зачем ты пришёл

Ха. Если бы ты только это не понял...

А вот это использование и корректность типов при этом вполне проверяется тестами

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

Я ещё раз повторяю: то что проверено в типах проверять смысла нет. Это область компилятора. В компиляторе могу быть ошибки, конечно, но я думаю это достаточно редкое явление, чтобы не считать его основным.

И если более-менее осмысленная программа на хаскеле скомпилировалась, это часто значит что она работает корректно. Часто в том смысле что несравнимо чаще чем с++, си, php, javascript в той же ситуации.

То что корректно в динамическом языке - мне пофиг, потому что это не имеет практического смысла.

Ещё раз - смысл в том чтобы возложить возможно большее число проверок на типы, потому что типы проще в написании и поддержке.

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

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