Тут написано, что 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 прав, это совсем другое. Одна из проблем велфера ещё в том, что он делает помск работы на начальном этапе невыгодным, проще ничего не делать. Так что тут проблема не в людях, они ведут себя экономически целесообразно в рамках предложенных условий.
Извините, не было времени на подробное изучение этого аспекта, я предпочитаю учиться самостоятельно.
Пожалуй, не буду дальше читать, предпочитаю учиться самостоятельно.