Вы намекаете, что эти тысячи тикетов никто из разработчиков даже не прочитал? Если хоть кто-то хоть раз прочитал, то тип тикета точно актуален, это меняется за секунду.
Саблайм и Атом для больших проектов — это немного не то как-бы) IDE не зря придумали всё-таки.
С одной стороны — да. А с другой — Rubymine, сколько не пробовал её в своих проектах, тупо виснет по несколько раз в час (причём может целую минуту висеть несмотря на 16 Gb оперативы) и получается, что она наоборот подходит только для относительно мелких проектов. В то время как Sublime справляется на ура с большими проектами.
Я бы проголосовал за то, чтобы в компании на какое-то время заморозили разработку новых фич и занялись исправлением ошибок и, самое главное, рефакторингом кода и/или производственного процесса
Этого, конечно, не будет, т.к. одни только багфиксы по платной подписке — это чересчур. Отдел маркетинга будет в шоке, да и пользователи, которых сейчас всё устраивает, тоже. Так что в лучшем случае больший процент времени на эти вещи смогут выделить.
Думаю, что проблема в том, что npm пытаются сравнивать с Maven, PyPI или RubyGems, в которых мусор не приветствуется. В npm же Эшли Уильямс (да и не только она) практически призывает постить всё подряд. По факту никому не интересно сколько пакетов в хранилище. Интересно сколько из них полезных… Это косвенно можно оценить по количеству скачиваний за месяц, допустим более 100 или более 1000 раз.
В принципе, даже если просто исходить из предпосылки, что полезный пакет решает какую-то обобщенную практическую задачу, то их количество ограниченно сверху тысячами, пусть будут представлены разные подходы к решению каждой задачи — всё равно остаётся ограничение в десятки тысяч. Всё что сверх этого, либо устаревшие пакеты, либо тот самый мусор, который всё же есть везде, просто в меньшем процентном соотношении. Чтобы показать крутость npm надо не циферками меряться, а составить список практических задач, для которых есть решения в npm, а в других хранилищах подобных пакетов нет.
Впрочем, тут есть ещё один феномен npm, который заключается в моде на пакеты с одной/двумя функциями. Это не укладывается в привычное понимание библиотеки, поэтому если сравнивать с другими хранилищами пакетов, то такие пакеты надо считать отдельно. Иначе какой смысл сравнивать тёплое с мягким на графиках?
Так это правда, доля программистов, которые всерьёз занимаются разработкой библиотек, довольно мала во всех языках. Но если в других языках остальные просто не публикуют никаких пакетов, то npm поставил своей целью, чтобы каждый, кто хоть неделю изучал JS, обязательно опубликовал какой-нибудь пакет. Они так прямо и говорят: хотим 15 миллионов авторов в npm и пофиг, что программистов в мире всего 18 миллионов. Можешь хотя бы пару строчек на JS написать — срочно делай пакет, мы ждём тебя!
Ну, Вы ворвались в ветку с заявлениями типа формальное описание — это бриф, а формальное доказательство — то же самое, что тестирование. Исходя из этого сложно сделать вывод, что тема Вам хоть капельку интересна, т.к. все заявления мимо кассы.
На самом деле тема очень обширная. Хоть пока и не мейнстримная. И то, что Eiffel, Coq и Prolog не используются широко в повседневной разработке вовсе не значит, что они умерли, идеи их живут и развиваются. Рано или поздно это всё придёт и в мейнстрим, т.к. цена ошибок в ПО с каждым годом только растёт.
Вам не кажется забавным, что эта "пустопорожняя беседа" по большей части состоит из Ваших собственных комментариев, на которые Вам изредка отвечают разные люди?
А по поводу ссылок, я Вам дал ссылки на Agda, на символьное выполнение программ и т.п. Уже успели ознакомиться?
В качестве практического применения символьное выполнение используется для автоматической генерации юнит-тестов.
Что касается Agda, то на основе его идей пилят язык общего назначения Idris, в феврале версию 1.0 собираются зарелизить.
А Вы ждали развития теории формального доказательства в комментариях на Хабре?.. смешной Вы однако.
Когда Вы уже ветку с начала перечитаете и осознаете, что тут никто и не собирался никаких задач ставить.
Сформулируйте лучше цель вашего активного оффтопика… Вы хотите привести доказательство, что формальная верификация невозможна никогда и ни при каких условиях или тупо покапитанить что это долго, дорого и не во всех случаях возможно?
Это сродни найти доказательство теоремы, что ничуть не проще нахождения конкретного решения, а даже — наоборот, сложнее.
Естественно написать корректную (с гарантированным отсутствием багов) программу сложнее, чем некорректную. И, разумеется, писать корректные программы экономически невыгодно, по крайней мере на текущем этапе развития индустрии. Какой смысл в ваших капитанских вопросах не по теме?
А практический смысл формальной верификации — то самое ПО без багов, пусть пока в теории. Но если не развивать теорию, то оно никогда в реальности и не появится.
Вы умеете внимательно читать? Перечитайте, пожалуйста, эту ветку с начала и поймите, что тут обсуждают теоретическую возможность формального доказательства при условии неограниченного времени и бюджета, а не его практическую целесообразность.
но вам об этом не сообщили, вы всё равно с порога будете утверждать, что наверняка программа ошибочная?
Вы меняете условия на ходу. Обсуждался случай, когда достоверно известно об отсутствии формального описания, цитата: "Если нет формального описания, то ошибок тоже нет?"
Хм, а кто-то всерьёз начнёт доказывать, что их программа безошибочна? Отсутствие формального описания означает наличие N неизвестных ошибок в программе, где N нелинейно растёт вслед за ростом сложности, объёма кода и т.д. Учитывая невозможность обнаружения всех N ошибок без формального описания, действительно можно сказать, что вся программа ошибочна.
Вообще говоря, в описании реального мира математика продвинулась куда дальше, чем программирование (см. математическая физика). Но по сути и то и то работает с упрощенными моделями реальности. Формальное описание — это и есть модель.
Теперь вопрос — можем ли мы (как вид) создать безбажное формальное описание нетривиального продукта?
Да можем конечно… С математикой же мы как вид как-то справляемся. Так же и программа может быть представлена в декларативном виде. Есть особо сложные случаи, но подавляющее большинство программ реально формализовать… Другой вопрос, что это кучу времени займёт при текущем состоянии IT-индустрии (что не говори, а она ещё только на начальном уровне развития).
Не тупите… Навешивание ярлыков — это оскорбление, подшучивание над уровнем — нет. Тем более единственный актуальный для Вашего друга ярлык — дохляк, остальное никаким боком к физической форме не относится.
В любом случае от ярлыков позитивного воздействия нет, Вы могли бы ему, допустим, в ситуации когда надо что-то тяжёлое переставлять, попросить его переставить что-то совсем лёгкое с намёком, что большее он не поднимет. Это было бы буквальной аналогией с примером из статьи.
Фишка в том, что уровень в чем бы то ни было не является константной характеристикой человека и практически всегда может быть улучшен. Дружеские подколы способствуют этому улучшению, а оскорбления и навешивания ярлыков лишь показывают духовную незрелость оскорбляющего и его неуверенность в себе.
Вы намекаете, что эти тысячи тикетов никто из разработчиков даже не прочитал? Если хоть кто-то хоть раз прочитал, то тип тикета точно актуален, это меняется за секунду.
С одной стороны — да. А с другой — Rubymine, сколько не пробовал её в своих проектах, тупо виснет по несколько раз в час (причём может целую минуту висеть несмотря на 16 Gb оперативы) и получается, что она наоборот подходит только для относительно мелких проектов. В то время как Sublime справляется на ура с большими проектами.
Этого, конечно, не будет, т.к. одни только багфиксы по платной подписке — это чересчур. Отдел маркетинга будет в шоке, да и пользователи, которых сейчас всё устраивает, тоже. Так что в лучшем случае больший процент времени на эти вещи смогут выделить.
Думаю, что проблема в том, что npm пытаются сравнивать с Maven, PyPI или RubyGems, в которых мусор не приветствуется. В npm же Эшли Уильямс (да и не только она) практически призывает постить всё подряд. По факту никому не интересно сколько пакетов в хранилище. Интересно сколько из них полезных… Это косвенно можно оценить по количеству скачиваний за месяц, допустим более 100 или более 1000 раз.
В принципе, даже если просто исходить из предпосылки, что полезный пакет решает какую-то обобщенную практическую задачу, то их количество ограниченно сверху тысячами, пусть будут представлены разные подходы к решению каждой задачи — всё равно остаётся ограничение в десятки тысяч. Всё что сверх этого, либо устаревшие пакеты, либо тот самый мусор, который всё же есть везде, просто в меньшем процентном соотношении. Чтобы показать крутость npm надо не циферками меряться, а составить список практических задач, для которых есть решения в npm, а в других хранилищах подобных пакетов нет.
Впрочем, тут есть ещё один феномен npm, который заключается в моде на пакеты с одной/двумя функциями. Это не укладывается в привычное понимание библиотеки, поэтому если сравнивать с другими хранилищами пакетов, то такие пакеты надо считать отдельно. Иначе какой смысл сравнивать тёплое с мягким на графиках?
Так это правда, доля программистов, которые всерьёз занимаются разработкой библиотек, довольно мала во всех языках. Но если в других языках остальные просто не публикуют никаких пакетов, то npm поставил своей целью, чтобы каждый, кто хоть неделю изучал JS, обязательно опубликовал какой-нибудь пакет. Они так прямо и говорят: хотим 15 миллионов авторов в npm и пофиг, что программистов в мире всего 18 миллионов. Можешь хотя бы пару строчек на JS написать — срочно делай пакет, мы ждём тебя!
Ну, Вы ворвались в ветку с заявлениями типа формальное описание — это бриф, а формальное доказательство — то же самое, что тестирование. Исходя из этого сложно сделать вывод, что тема Вам хоть капельку интересна, т.к. все заявления мимо кассы.
На самом деле тема очень обширная. Хоть пока и не мейнстримная. И то, что Eiffel, Coq и Prolog не используются широко в повседневной разработке вовсе не значит, что они умерли, идеи их живут и развиваются. Рано или поздно это всё придёт и в мейнстрим, т.к. цена ошибок в ПО с каждым годом только растёт.
Вам не кажется забавным, что эта "пустопорожняя беседа" по большей части состоит из Ваших собственных комментариев, на которые Вам изредка отвечают разные люди?
А по поводу ссылок, я Вам дал ссылки на Agda, на символьное выполнение программ и т.п. Уже успели ознакомиться?
В качестве практического применения символьное выполнение используется для автоматической генерации юнит-тестов.
Что касается Agda, то на основе его идей пилят язык общего назначения Idris, в феврале версию 1.0 собираются зарелизить.
А Вы ждали развития теории формального доказательства в комментариях на Хабре?.. смешной Вы однако.
Когда Вы уже ветку с начала перечитаете и осознаете, что тут никто и не собирался никаких задач ставить.
Сформулируйте лучше цель вашего активного оффтопика… Вы хотите привести доказательство, что формальная верификация невозможна никогда и ни при каких условиях или тупо покапитанить что это долго, дорого и не во всех случаях возможно?
Естественно написать корректную (с гарантированным отсутствием багов) программу сложнее, чем некорректную. И, разумеется, писать корректные программы экономически невыгодно, по крайней мере на текущем этапе развития индустрии. Какой смысл в ваших капитанских вопросах не по теме?
А практический смысл формальной верификации — то самое ПО без багов, пусть пока в теории. Но если не развивать теорию, то оно никогда в реальности и не появится.
Пример выше легко решается символьным вычислением.
Что-то Вы опять какую-то несуразицу написали… Понятно что Вам лень изучать Agda, Prolog и т.д. Но какой смысл оффтопить, когда Вы совсем не в теме?
Вы умеете внимательно читать? Перечитайте, пожалуйста, эту ветку с начала и поймите, что тут обсуждают теоретическую возможность формального доказательства при условии неограниченного времени и бюджета, а не его практическую целесообразность.
Вы меняете условия на ходу. Обсуждался случай, когда достоверно известно об отсутствии формального описания, цитата: "Если нет формального описания, то ошибок тоже нет?"
Хм, а кто-то всерьёз начнёт доказывать, что их программа безошибочна? Отсутствие формального описания означает наличие N неизвестных ошибок в программе, где N нелинейно растёт вслед за ростом сложности, объёма кода и т.д. Учитывая невозможность обнаружения всех N ошибок без формального описания, действительно можно сказать, что вся программа ошибочна.
Кхм, в этой ветке речь идёт о формальном доказательстве отсутствия ошибок в программах. А Вы говорите об обычной спецификации, это совсем другая тема.
Вообще говоря, в описании реального мира математика продвинулась куда дальше, чем программирование (см. математическая физика). Но по сути и то и то работает с упрощенными моделями реальности. Формальное описание — это и есть модель.
Да можем конечно… С математикой же мы как вид как-то справляемся. Так же и программа может быть представлена в декларативном виде. Есть особо сложные случаи, но подавляющее большинство программ реально формализовать… Другой вопрос, что это кучу времени займёт при текущем состоянии IT-индустрии (что не говори, а она ещё только на начальном уровне развития).
Деанонить человека по специально зареганному (12 января 2017 в 12:42) аккаунту — провальная идея.
Не тупите… Навешивание ярлыков — это оскорбление, подшучивание над уровнем — нет. Тем более единственный актуальный для Вашего друга ярлык — дохляк, остальное никаким боком к физической форме не относится.
В любом случае от ярлыков позитивного воздействия нет, Вы могли бы ему, допустим, в ситуации когда надо что-то тяжёлое переставлять, попросить его переставить что-то совсем лёгкое с намёком, что большее он не поднимет. Это было бы буквальной аналогией с примером из статьи.
Фишка в том, что уровень в чем бы то ни было не является константной характеристикой человека и практически всегда может быть улучшен. Дружеские подколы способствуют этому улучшению, а оскорбления и навешивания ярлыков лишь показывают духовную незрелость оскорбляющего и его неуверенность в себе.
Хм, этот отрывок ведь про Kanban, а не про Scrum.