Обсуждение:Доказательное программирование

Последнее сообщение: 13 лет назад от Tim2 в теме «ВП:МАРГ»

ВП:МАРГ править

Если честно, я не понимаю аргументов за оставление, приведённых в обсуждении от 11 января. Да, понятно, что Каймин преподает в московском вузе, рассказывая студентам про доказательное программирование. Да, его упоминал академик Ершов в 1 статье и докладе статье, в 1984 году. Достаточно ли этого для значимости? Список источников там, откуда передан текст, вообще не выдерживает никакой критики: «Ершов А. П. Теоретическое программирование. М.,Наука,1980.» имеет к ОИ «Доказательное программирование» такое же отношение, как и «Дейкстра Э. Дисциплина программирования. М.: Мир, 1978» — то есть никакое.

В статье много воды и наукообразия, много общих слов. «Действующий стандарт ГОСТ Р 51904-2002» не упоминает никаких доказательных программирований, зачем его приплели? "к этому подходу примыкают и частично пересекаются с ним такие известные подходы, " — какой АИ считает, что «доказательное программирование» «примыкает и пересекается» к современным методам формальной верификации программ? Г-н Каймин? Достаточно ли этого? Конечно, можно поступить согласно букве правила — удалить все утверждения о миллионных тиражах, утверждения без источников, утверждения, что Каймин наследует Флойду и Ершову (а заодно Эйлеру и Ленину, надо полагать), воду, и от статьи останется стаб в три строчки, который будет через полгода удалён. Но стоит ли это делать?

Я предлагаю повторно обсудить вопрос ВП:МАРГ, к удалению как маргинальную теорию. — Fluffy86 19:47, 11 сентября 2010 (UTC)Ответить

  • Тут есть много тем для обсуждения, но вопрос об отнесении идеи к числу маргинальных надо закрыть раз и навсегда. Если идею рассматривал президиум АН СССР и нашел ее важной и перспективной - то она уже никак не маргинальная, а наоборот - поддержанная научным сообществом. А то, что она в настоящее время находится в забвении - так это результат общих изменений в деятельности программистов за прошедшие 25 лет. Grig_siren 08:17, 24 января 2011 (UTC)Ответить
  • "какой АИ считает, что «доказательное программирование» «примыкает и пересекается» к современным методам формальной верификации программ?" - из того, что написано в статье о «доказательном программировании», ясно видно сходство (может быть, неполное, может, внешнее) с упомянутой верификацией, ГОСТом, защищенным программированием и т.д. Это сходство в статье должно быть отмечено, даже если нигде в АИ такого не отмечалось. Иначе, что получается - актуальность данный подход утратил, но замены ему нет? Подобные самоочевидные выводы не требуют АИ.--tim2 14:48, 24 января 2011 (UTC)Ответить