ЛОР, помоги выбрать ЯП для обучения

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

1. Выливает воду из чайника что сводит задачу к уже решенной

Получается, что программист херово декомпозировал предыдущую задачу и поэтому наговнокодил.

иван степанычем называет и себя, и кота, и письменный шкаф

Не знаю, что такое письменный шкаф и кто такой Иван Степаныч, но про кота согласен.

???

Не понял. Чем статическая проверка типа значений в функциях и переменноых

string-ref : String Int -> Char
pi : Real

отличается от назначения именам string-ref и pi стабильных типов?

стадно не понимать, что письменный шкаф, это функциональная композиция книжного шкафа и письменного стола.

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

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

Когда-то были языки программирования с несколькими точками входа в процедуру. Фортран с Entry; Бейсик с GOSUB, которым можно было начать выполнение подпрограммы с любой строки. Потом сказали, что это очень путает.

Чем статическая проверка типа значений в функциях и переменных … отличается от назначения именам … стабильных типов?

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

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

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

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

То есть натурально fill-pot, heat-pot и собранные из них (def heat-the-full-pot heat-pot), (def heat-the-empty-pot (comp heat-pot fill-pot).

Понятно, красиво, расширяемо.

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

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

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

это и есть основная задача и ценность типизации

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

Или ты как тот программист с чайником? %)

1. Научится понимать цель
2. Определить срок с учетом потерь.
3. Научится декомпозировать цель на задачи.
4. Научится понимать какие алгоритмы приведут к решению задач.
5. Расписать в блокноте поблочно какими техническими возможностями будешь достигать поставленной цели.
6. Перестать постить на ЛОРе всякую хрень.
7. Четко разбитьработу на этапы и сроки.
8. Приступить к реализации.
9. Контролировать себя ежедневно.
10. Проводить презентации для заинтерессованный еженедельно. А-ля «возможности технологии которую я выбрал!»

Но ты ведь согласен, что написание кода и автоматическая проверка его на корректность — это разные задачи? %)

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

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

есть понятие - написание корректного кода, то есть кода проходящего проверки корректности

Но ведь ты можешь делать это вручную, просто у себя в голове. Без всякой статической типизации %) Ведь

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

просто у себя в голове.

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

этак вы еще денег потребуете за программирование в голове.

на отдельные функции наполнение чайника и его нагрев

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

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

В How to Design Programs типы вообще в комментариях. Автоматическая проверка типов просто помогает избежать случайных ошибок. И вообще, зачем что-то делать вручную, если это легко может сделать компьютер? Так-то можно и программу компилировать вручную без make и даже переписывать из языка программирования в машинный код вручную.

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

Если код прошёл проверку типизации, это ничего не говорит о его корректности. Он также может содержать ошибку.

дом должно строить не абы как, а чтобы он не рухнул при эксплуатации.

И аналогом типизации являются акты стройнадзора. Есть индивидуальное строительство безо всяких актов, есть здания с актами, которые упали. Гарантий наличие акта не даёт.

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

Это так, никто и не спорит.

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

Если компьютер может сделать это полностью без твоего участия — то да, незачем. Вот сборка мусора происходит полностью автоматически и на неё ученику отвлекаться не нужно; со статической типизацией не так — аннотации типов в общем случае сами себя не расставят, и придётся отвлекаться от главной задачи — освоения принципов проектирования программ — на неравную борьбу с системой типов.

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

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

// Для любых A, B, C
// compose(f : B -> C, g : A -> B) : (A -> C)
auto compose (auto f, auto g)
{
...
}

Если код прошёл проверку типизации, это ничего не говорит о его корректности.

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

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

да не бойтесь вы этих типов, нервус. они сами вас боятся.

но в отношении частичной корректности относительно неких правил - говорит. и чем больше таких правил - тем более код частично корректен

Вот этот подход и отвращает от статической типизации. «Частично корректный код» это как рыба «второй свежести». Если тип sin : Double -> Double, то пройденная типизация никак не поможет нам узнать, действительно ли эта функция для всех значения своего аргумента возвращает синус этого значения.

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

На практике, из-за огромной сложности полных императивных инструкций их пишут в урезанном виде

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

Зачем этот ASCII ART?

Я имел в виду строчки или квадраты из звездочек(с комментарием внутри) между функциями чтобы более заметно отделить их одну от другой. Сам всегда это визуальное выделение использую.

Лучше бы вместо него вставляли #pragma region, которые понимают редакторы.

Видимо понимающие редакторы не так часто встречаются.

Если править код придется на другой машине

я считаю что такие ситуации можно игнорировать.

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

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

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

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

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

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

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

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

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

вы рассуждаете обывательски.

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

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

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

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

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

В How to Design Programs помогает.

Хорошая книга. Вот еще если бы там в примерах язык был использован не лиспоподобный,а более человекочитаемый…

Аннотации типов надо ставить в любом случае

Конечно, нужно понимать, какой формы данные приходят в твою функцию на вход и что должно получиться на выходе. В комментариях описать — отлично.

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

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

Дело привычки же. Многих после лиспов от любого другого синтаксиса начинает подташнивать.

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

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

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

Значит, придётся дробить. Или страдать %)

Мне кажется, то что вы делаете, вы делаете совершенно зря. Для того, чтобы думать на такую тему, нужно получить определённую базу. Обычно её дают на первых двух-четырёх курсах любой технической специальности. А без этого один позор да поношение выходят. Я честно скажу, что последние лет двадцать о трансцендентых числах не задумывался, чтобы о них подумать мне нужно: а) обновить свои университетские знания; б) приобрести новые университетские знания, бо нас больше по матану гоняли, уравнения в частных производных инженеру нужны, а теория чисел — факультативны. Но у меня нет ни времени, ни желания. Поэтому я со спокойной совестью промолчу. Чего и вам желаю. А я вам желаю добра, я на вашей стороне, честно.

И это хорошо что фигушки

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

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

И тут в тему с ноги влетают прогрессивная технология STM. Человеческий мозг не приспособлен следить за мьютексами. Точно так же как не приспособлен находить независимые участки в императивной спецификации. Мы это можем, но тяжело, медленно и с ошибками. А вот компьютеры — запросто, так что пускай они этим и занимаются.

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

Ну, всё таки попытайтесь. Допустим мне нужно доехать от Красной Площади, до Третьяковской галереи это недалеко, так что инструкция должна выйти короткая.

Если мир у нас один то вычисляем его следующее состояние,а не новый мир.

Это в императивной парадигме. Вот, возьмём факториал

int fac = 1
for{i = 1; i<N; i++} fac *= i

здесь у нас есть объект — факториал, у него есть состояние, мы его меняем и, если не накосячили, то после всех изменений он придёт в нужное состояние

(define (fac n acc)
  (if (<= n 1) acc
    (fac (- n 1) (* n acc))))

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

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

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

Если код прошёл проверку типизации, это ничего не говорит о его корректности. Он также может содержать ошибку.

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

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

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

Это как обучение правильным приемым работы с любым инструментом на производстве. Они позволяют выполнять работу и более качественно и безопасно.

Во-первых это всё не технические навыки.

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

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

Отличное оправдание для неудачников. Если у юноши нет девушки, то перед нами либо монах, либо человек с проблемами. Монахи бывают, видел, общался, совсем исключать такой случай не следует, но … если на батин вопрос: „Когда уже девушку найдёшь“, у вас нету подходящего ответа, нужно не о высоком рассуждать, а пойти помыться что ли, одежду непозорную купить, с пуза пару [десятков] килограмм сброить и т.п. А монахи есть и святые люди-бессеребрянники. Только, говоря о социальном слое инженеры-технари, это всё не имеет никакого значения.

вот не было беды… но пришли математики…

Это вы ещё тестировщиков не видели. Тогда бы у меня могло быть nil, true, -3, "3", "3яйца", "три яйца", [3] или 3.0 яиц. И это только первое что на ум приходит.

trade vs craft

и таки да деньги это скаляр

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

Это документирование интерфейса функции.

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

Например в Аде можно в параметрах функции указать не только их тип,но и «направление передачи». Если параметр «in» то он только передается в функцию. А если «in out» то функция может его изменить там откуда она вызывалась.

«крах социума» не лобио покушать

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

ща 20 век какой то алтернативный получился

см Либеральный Фашизм ( книжка поздних нулевых)

очередное баре ругаются у холопов чубы трешать

в реальной реальности Кайзер рейх продолжал социалдемократию после завершение очередным мирным договор замятни 1914(если оно вообще было)

Вудро Вилсон тот ещё Евгений

инженеры - дети в позднем союзе это безотцовщина услившаяся вел-отеч - но не начатая ею :(

Вот этот подход и отвращает от статической типизации. «Частично корректный код» это как рыба «второй свежести».

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

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

1Сники проекты на миллионы строк пишут с динамической типизацией. Типы есть, но только в комментариях.

И я бы в тот момент был рад если бы мне кто-то объяснил это сразу,без необходимости доходить самому методом тыка. Но это было в начале 90х - объяснять было особо некому.

Синдром утёнка. Я с Паскаля на Си переходил и тоже сначала было неудобно.

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

Это лишь одна_из оценок. Показывает активность работы ученого - и не более того. Ошибаться может и тот кто десять статей опубликовал и тот кто опубликовал одну. Но вот если опубликовал одну статью за десять лет - то очевидно что эта тема ему не интересна и звать его на симпозиум по ней нет смысла.

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

Выбрать уже описанный тип из доступных разве сложно?

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

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

Значит, придётся дробить. Или страдать %)

Видел игру Жизнь, разбитую на 21 класс. По мне, так проще просто переписывать с нуля при каждом изменении задачи, чем такую нечитаемую лапшу производить.

По этой теме: https://habr.com/ru/articles/153225/ и https://eax.me/haskell-bread-task/