Программист: математика не нужна, нужно приносить велью
=
Архитектор: сопромат не нужен, нужно приносить велью

Она была неплоха, но концовка все смазала

Программы это типы и велью, у программиста фиксированная производительность, если он пишет типы, то он делает меньше велью

:) вспоминается старое фидошное про сумму разума на планете (почему-то)

Что занимает больше времени : исправление ошибок бизнес логики или исправление ошибок компиляции?

исправление ложных дихотомий)

холивары в чатике

Как то же надо оценивать время на задачу. Я серьёзно спрашиваю.

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

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

Поэтому, как верно заметил @niquola, давайте сохранять дружественность беседы.

Ладно бы показали что, а голословные утверждения уже выглядят дико.

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

В первую очередь компилятору

Прувмиронг!

Антон же показывал.

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

Но копаться в программе с lldb было веселее, поэтому просто задал один вопрос, ответ на который меня устроил

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

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

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

а вот ошибки бизнес логики это вообще нечто!