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

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

Я считаю, что coq-еры должны доказывать

(Денис, я прошу прощения заранее за использование сообщения в юмористических целях, очень уж хороший шаблон получился)

Позвольте изложить одну мысль. Всё чаще я наблюдаю, в различных сообществах, что к coq-ерам есть такое отношение, будто бы они должны (!) что-то кому-то доказывать. Друзья, мы никому и ничего не должны доказывать. Мы оставляем за собой право использовать то, что нам удобно и то, что делает нашу работу эффективнее. Другие имеют право использовать то, что удобнее для них. Даешь Admitted в массы!

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

Вот если бы я сегодня пришёл в команду к Кложуристам и заявил им: "Знаете, ваша Кложа - это полная фигня, вам нужно выкинуть весь ваш код и переписать всё на Хаскеле!" - вот в этом случае да, я должен был бы доказывать, и именно потому, что речь идёт о призыве. В данном же случае, затронув тему о типах, я никого ни к чему не призывал.

(Денис, я прошу прощения заранее за использование сообщения в юмористических целях, очень уж хороший шаблон получился)

Позвольте изложить одну мысль. Всё чаще я наблюдаю, в различных сообществах, что к coq-ерам есть такое отношение, будто бы они должны (!) что-то кому-то доказывать. Друзья, мы никому и ничего не должны доказывать. Мы оставляем за собой право использовать то, что нам удобно и то, что делает нашу работу эффективнее. Другие имеют право использовать то, что удобнее для них. Даешь Admitted в массы!

У кокеров работа такая — доказывать, а в хаскелле логика неконсистентная, там доказать ничего и нельзя дальше чем "мамой клянусь"

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

Не дай бог кложуристы будут писать Self Driving AI

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