Погодите, это всё интересные мысли, но это всего лишь мысли. У меня есть конкретная задача: дать студентам пощупать model checking. Я иду в Википедию и смотрю список реальных инструментов. Их там десятки. Использовать Haskell на практике никому в голову не приходит. При этом очень часто разрабатывают какой-то собственный формализм, вовсе даже не в функциональном стиле.
Тут написано, что Haskell оказался удобен для решения конкретной задачи верификации микроядра, но из этого не следует, что условная Promela была бы хуже.
Университет не может переориентировать курсы каждые три-четыре года в соответствии с модой. Кроме того, конкретная парадигма в принципе может отсутствовать с списке модных языков по 10-20 лет. Поэтому брать приходится более-менее известные языки, у которых есть перспектива не помереть в ближайшем будущем.
А откуда вообще эта идея? Мне и вправду интересно. Только не на уровне теорий, а конкретных продуктов, которыми можно воспользоваться.
Я немного рассказываю студентам про model checking, вот в своё время пытался подобрать наиболее простой инструмент, и в итоге выбрал банальный Spin. Если посмотреть список в Википедии, Хаскелл там вообще не упоминается, да и, по правде говоря, больше половины указанных проектов реально мертвы.
Честно говоря, не уверен. Скажем, в многопоточном программировании обычно используется какой-нибудь облегчённый язык моделирования (напр., Promela — вполне себе императивный), на котором пишется алгоритм, а потом уже всё это переписывается на обычном языке. В конце концов, и в Haskell есть «нечистые» функции вроде генератора случайных чисел или чтения ввода пользователя.
Я с этой темой знаком поверхностно, и мне показалось, что тут важнее не какой язык, а что мы ищем. Ну и, соответственно, сложность зависит от этого. Например, если вам надо доказать, что в системе есть deadlock, это ещё терпимо, т.к. достаточно найти один пример того, как это может случиться. А вот если требуется доказать, что всегда после события А рано или поздно наступает событие B, это уже куда сложнее.
Я не готов судить, но вполне вероятно, что имеется таки, по крайней мере, один тектонический сдвиг, о котором говорит Сассман:
«Программирование сегодня больше напоминает науку: вы берете часть библиотеки и «тыкаете» в нее — смотрите на то, что она делает. Затем вы спрашиваете себя, «Могу ли я настроить это так, чтобы оно делало то, что мне нужно?». Подход «анализ через синтез», используемый в SICP, когда вы строите большую систему из простых, маленьких частей, стал неактуальным. Сегодня мы программируем «методом тыка».
То есть дело не только в том, что в 2000-м году резко потребовались верстальщики HTML, а в 2015-м — писатели на Angular, и рынку приходится иметь дело с существующими людьми, какими бы они ни были, но и в более серьёзных изменениях.
Скажем, что классические методики SE говорят о ситуациях такого вида:
— Мне нужно использовать библиотеку, в которой есть заведомый баг, но варианта не использовать её у меня нет?
— Мне нужно использовать библиотеку, чья структура плохо совместима с архитектурой моей системы?
— Две библиотеки предоставляют массу дублирующегося, плохо документированного или просто legacy в худшем смысле слова кода?
Я могу придумать массу таких вот вопросов, которыми в науке мало кто задаётся, потому что это скучно и на премию Тьюринга не потянет.
Любая программа на любом языке может быть представлена диаграммой состояний с переходами и, соответственно, можно доказать/опровергнуть требуемое поведение. Математическая чистота тут не при чём. В Хаскеле используется исчисление рекурсивных функций, а в С++ (например) — теория автоматов.
улучшение существующих языков за последние 20 лет — прямое следствие именно такого алармизма и именно таких (действующих) людей
Думаю, что причины не только в этом, но и не без того. Впрочем, мы тут обсуждаем конкретный текст, а не то, как взгляды автора помогли ему в его работе :)
будет ли расти давление на средних специалистов, или это как раз тот случай, где принципиально поменять ситуацию не получится
Может, я сейчас слишком копну, ну да ладно. Вот есть «дискурс первого уровня». Броуди в «Thinking Forth» пишет, что паттерны проектирования нужны прежде всего для того, чтобы биться с проблемами, вызванными самими (плохими) языками программирования. Дейкстра очень прохладно отзывается о software engineering. Он-то считал, что если нормально доказывать корректность алгоритмов, то всё и будет работать (справедливости ради, он по факту критикует отдельные части SE, а не всё подряд).
Сообщество Мейера делает переход на следующий уровень: да, нереалистично надеяться на то, что у нас будут идеальные языки и все будут математически доказывать корректность, но давайте хотя бы разработаем разумную методику процесса.
Это справедливо (как и ремарки Дейкстры), но давайте перейдём к третьему уровню. Если совсем упростить, можно почти всё свести к экономической целесообразности. Хорошо обученный специалист затратил долгие годы на своё образование и стоит достаточно дорого. Проектирование и поддержка качественной системы тоже стоит денег (да, считается, что это окупается, но гарантий нет), при этом цена ошибки далеко не всегда измеряется миллионами. Вот мы и подсчитываем, стоит оно того или нет.
Я думаю, что качество (в широких массах) двигается за счёт качественных компонентов, которые достаются дёшево. Например, вас беспокоит сохранность данных при передаче. Ну окей, переходим на HTTPS — благо есть готовые библиотеки, разбираться с протоколом не нужно. Или хотим мы создать качественный 3D мир. Прекрасно, берём Unity, там уже всё есть. То есть я в целом хочу сказать, что методика нужна, но надеяться на повсеместное применение лучших практик невозможно, потому что это отнюдь не даром достаётся.
Это действительно какой-то поток сознания и алармизм (да, я в курсе замечательных достижений автора вне общих рассуждений). Людей, двигающих вперёд software engineering в процентах мало, как и выращивающих пшеницу, но человечеству, видимо, хватает. Лучшие идеи теории SE либо уже воплощены в существующих языках (они заставляют даже новичков писать лучше, чем 20 лет назад), либо объективно сложны для среднего специалиста. Продолжать работать в этом направлении надо, но принципиально поменять ситуацию вряд ли получится, слишком много здесь нетехнических факторов. Я не думаю, что спутник упал из-за недостаточного количества профессоров SE в университетах. Гораздо вероятнее, что конкретный сотрудник оказался недостаточно внимательным (допустил баг), а другой достаточно ленивым или недостаточно компетентным для работы по приёмке качества.
Как писал Пушкин, «Здравствуй, племя / Младое, незнакомое!»
Дети всегда уже не наши, а свои собственные. Новое поколение, новая и культура, даже в рамках одной страны.
Но в целом драматизируете, ребёнку 5 лет, пока такого не заметил, хотя он вполне погружён в местную жизнь.
Да, похоже на то. Ну штука в том, что кое-где (в тех же Штатах, да и в России) айтишники часто оказываются в своей собственной ценовой категории, отличаясь от инженеров в других областях. В Японии, кажется, что это не так: вероятно, что зарплаты по области и вправду выше, но с американскими никак не сравнить.
Восемь лет в Японии, полёт нормальный.
В целом чем дольше живу, тем менее экзотичной страна кажется. Теперь даже странновато читать, что для кого-то тут «экзотика», по мне так уже всё логично и понятно :)
Основная масса странностей либо имеет разумные причины, либо «так сложилось исторически» опять-таки по понятным причинам, и местные тоже далеко не от всего в восторге. Короче говоря, как и везде в мире, свои достоинства и недостатки.
Насколько я знаю, у айтишников здесь далеко не запредельные зарплаты, так что если ехать, то ради конкретного проекта или общего интереса к стране.
Смотрите, я по сути высказываюсь в том ключе, что меня в основной работе мало волнует мнение коллег по вопросам специализации и т.п. Вероятно, Англия культурно достаточно далека от России, но Япония это вообще отдельная планета, и тем не менее. Я пишу статью, посылаю её в журнал, ну и всё. Допустим, коллеге она бы не понравилась, но мне-то до этого дела нет вовсе. Если кто-то не хочет затрагивать «чужую» тему — ну и ради бога, не навязывать же ему своё мнение.
В этом смысле, если вы правы (допустим, я не берусь судить), касается данная проблема в основном зависимых от начальства аспирантов, постдоков и тому подобных людей.
Computer science, AI и смежные области (иногда выхожу в образование, иногда в лингвистику, всякое бывает). Япония.
Вопрос на самом деле в том, кто конкретно вас (ну или гипотетического автора) может критиковать за «чужеродность» доказательств. В науке как и везде железно работает правило «не работать с чудаками». Мои работы оценивают почти исключительно рецензенты журналов и конференций. В свою очередь, журналы опираются на достаточно широкий пул людей, и крайне редко бывает, чтобы на мою работу прислали, скажем, три рецензии, и все бы они были в равной степени неадекватными. Иногда находится один ненормальный (из трёх), но в этом случае и мне, и принимающему решение редактору видно, что он выпадает из общего списка. Если же прямо все там со странностями, я просто забываю об этом журнале, благо мест, где публиковаться, сейчас навалом. В этом смысле моё месторасположение никакого значения не имеет, по факту я достаточно редко попадаю на японские конференции.
Может, он другим помогает в других задачах, а коммитят они. Да тут как бы kpi и не особо нужны: дают тебе задания, тв с ними справляешься или нет. В общем-то всегда можно понять, тобой субъективно довольны или не особо.
Не знаю, примерно 10 лет работаю в университете, публикуюсь регулярно, не сталкивался. Есть, скажем так, культурные различия в областях, но это несколько о другом.
которые были когда-то очень хороши в какой-то области знаний, но вместо того, чтобы учиться чему-то новому
Проблема часто бывает не в людях, а всё-таки в технологии и её внедрении. Олдскульный специалист потратил многие годы для того, чтобы стать профессионалом в своём наборе технологий и рабочих практик. Переход на новые обязательно означает некоторый временный провал, поэтому совершенно рациональным поведением будет не делать этого, если мы не ожидаем в итоге существенного роста производительности. А он не всегда есть, т.к. многие новые технологии (не все, конечно) являются эволюционным развитием старых и лишь немного модернизируют процесс.
EvilGenius18 прав, это совсем другое. Одна из проблем велфера ещё в том, что он делает помск работы на начальном этапе невыгодным, проще ничего не делать. Так что тут проблема не в людях, они ведут себя экономически целесообразно в рамках предложенных условий.
Я немного рассказываю студентам про model checking, вот в своё время пытался подобрать наиболее простой инструмент, и в итоге выбрал банальный Spin. Если посмотреть список в Википедии, Хаскелл там вообще не упоминается, да и, по правде говоря, больше половины указанных проектов реально мертвы.
Я с этой темой знаком поверхностно, и мне показалось, что тут важнее не какой язык, а что мы ищем. Ну и, соответственно, сложность зависит от этого. Например, если вам надо доказать, что в системе есть deadlock, это ещё терпимо, т.к. достаточно найти один пример того, как это может случиться. А вот если требуется доказать, что всегда после события А рано или поздно наступает событие B, это уже куда сложнее.
То есть дело не только в том, что в 2000-м году резко потребовались верстальщики HTML, а в 2015-м — писатели на Angular, и рынку приходится иметь дело с существующими людьми, какими бы они ни были, но и в более серьёзных изменениях.
Скажем, что классические методики SE говорят о ситуациях такого вида:
— Мне нужно использовать библиотеку, в которой есть заведомый баг, но варианта не использовать её у меня нет?
— Мне нужно использовать библиотеку, чья структура плохо совместима с архитектурой моей системы?
— Две библиотеки предоставляют массу дублирующегося, плохо документированного или просто legacy в худшем смысле слова кода?
Я могу придумать массу таких вот вопросов, которыми в науке мало кто задаётся, потому что это скучно и на премию Тьюринга не потянет.
Думаю, что причины не только в этом, но и не без того. Впрочем, мы тут обсуждаем конкретный текст, а не то, как взгляды автора помогли ему в его работе :)
Может, я сейчас слишком копну, ну да ладно. Вот есть «дискурс первого уровня». Броуди в «Thinking Forth» пишет, что паттерны проектирования нужны прежде всего для того, чтобы биться с проблемами, вызванными самими (плохими) языками программирования. Дейкстра очень прохладно отзывается о software engineering. Он-то считал, что если нормально доказывать корректность алгоритмов, то всё и будет работать (справедливости ради, он по факту критикует отдельные части SE, а не всё подряд).
Сообщество Мейера делает переход на следующий уровень: да, нереалистично надеяться на то, что у нас будут идеальные языки и все будут математически доказывать корректность, но давайте хотя бы разработаем разумную методику процесса.
Это справедливо (как и ремарки Дейкстры), но давайте перейдём к третьему уровню. Если совсем упростить, можно почти всё свести к экономической целесообразности. Хорошо обученный специалист затратил долгие годы на своё образование и стоит достаточно дорого. Проектирование и поддержка качественной системы тоже стоит денег (да, считается, что это окупается, но гарантий нет), при этом цена ошибки далеко не всегда измеряется миллионами. Вот мы и подсчитываем, стоит оно того или нет.
Я думаю, что качество (в широких массах) двигается за счёт качественных компонентов, которые достаются дёшево. Например, вас беспокоит сохранность данных при передаче. Ну окей, переходим на HTTPS — благо есть готовые библиотеки, разбираться с протоколом не нужно. Или хотим мы создать качественный 3D мир. Прекрасно, берём Unity, там уже всё есть. То есть я в целом хочу сказать, что методика нужна, но надеяться на повсеместное применение лучших практик невозможно, потому что это отнюдь не даром достаётся.
Дети всегда уже не наши, а свои собственные. Новое поколение, новая и культура, даже в рамках одной страны.
Но в целом драматизируете, ребёнку 5 лет, пока такого не заметил, хотя он вполне погружён в местную жизнь.
В целом чем дольше живу, тем менее экзотичной страна кажется. Теперь даже странновато читать, что для кого-то тут «экзотика», по мне так уже всё логично и понятно :)
Основная масса странностей либо имеет разумные причины, либо «так сложилось исторически» опять-таки по понятным причинам, и местные тоже далеко не от всего в восторге. Короче говоря, как и везде в мире, свои достоинства и недостатки.
Насколько я знаю, у айтишников здесь далеко не запредельные зарплаты, так что если ехать, то ради конкретного проекта или общего интереса к стране.
В этом смысле, если вы правы (допустим, я не берусь судить), касается данная проблема в основном зависимых от начальства аспирантов, постдоков и тому подобных людей.
Вопрос на самом деле в том, кто конкретно вас (ну или гипотетического автора) может критиковать за «чужеродность» доказательств. В науке как и везде железно работает правило «не работать с чудаками». Мои работы оценивают почти исключительно рецензенты журналов и конференций. В свою очередь, журналы опираются на достаточно широкий пул людей, и крайне редко бывает, чтобы на мою работу прислали, скажем, три рецензии, и все бы они были в равной степени неадекватными. Иногда находится один ненормальный (из трёх), но в этом случае и мне, и принимающему решение редактору видно, что он выпадает из общего списка. Если же прямо все там со странностями, я просто забываю об этом журнале, благо мест, где публиковаться, сейчас навалом. В этом смысле моё месторасположение никакого значения не имеет, по факту я достаточно редко попадаю на японские конференции.
Может, он другим помогает в других задачах, а коммитят они. Да тут как бы kpi и не особо нужны: дают тебе задания, тв с ними справляешься или нет. В общем-то всегда можно понять, тобой субъективно довольны или не особо.
Не знаю, примерно 10 лет работаю в университете, публикуюсь регулярно, не сталкивался. Есть, скажем так, культурные различия в областях, но это несколько о другом.
Проблема часто бывает не в людях, а всё-таки в технологии и её внедрении. Олдскульный специалист потратил многие годы для того, чтобы стать профессионалом в своём наборе технологий и рабочих практик. Переход на новые обязательно означает некоторый временный провал, поэтому совершенно рациональным поведением будет не делать этого, если мы не ожидаем в итоге существенного роста производительности. А он не всегда есть, т.к. многие новые технологии (не все, конечно) являются эволюционным развитием старых и лишь немного модернизируют процесс.
EvilGenius18 прав, это совсем другое. Одна из проблем велфера ещё в том, что он делает помск работы на начальном этапе невыгодным, проще ничего не делать. Так что тут проблема не в людях, они ведут себя экономически целесообразно в рамках предложенных условий.