kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Categories:

По поводу статьи Дэвиса еще:

http://elementy.ru/lib/164681/164687 и моего недавнего поста:
Сбудутся эти прогнозы или нет, но будущее чистой математики должно разительно отличаться от ее прошлого. В 1875 году любой грамотный математик мог полностью усвоить доказательства всех существовавших на тот период теорем за несколько месяцев. В 1975 году, за год до того, как была доказана теорема о четырех цветах, об этом уже не могло быть и речи, однако отдельные математики еще могли теоретически разобраться с доказательством любой известной теоремы. К 2075 году многие области чистой математики будут построены на использовании теорем, доказательства которых не сможет полностью понять ни один из живущих на Земле математиков — ни в одиночку, ни коллективными усилиями. Многие математики будут по-прежнему доказывать теоремы традиционными методами, но это будут уже лишь отдельные ностальгические островки в океане новой математической дисциплины. Будет широко применяться формальная проверка сложных доказательств, однако достижение общественного консенсуса будет столь же распространенным условием для принятия того или иного результата, что и строгое доказательство.
(вообще главку статьи по ссылке есть смысл прочитать целиком)

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

Первой и очень ранней попыткой справиться со сложностью были подпрограммы - а в конце 60-х в моду вошли самые разные методички по "организации совместной работы" - все эти "бригады главного программиста" и прочие уродцы (которые в современном мире реинкарнируются в виде всяких "экстремальных программирований" и проч).

Равно как и мода на формальные доказательства правильности программ примерно тогда пошла. Ущла видимо даже не потому что трудоемко, а потому что выяснился факт что формальное доказательство правильности не повышает особенно надежность - оно просто переносит риски в само доказательство и в формализацию задачи.

Так вот математики на данный момент застряли именно на этой стадии. Причем насколько я могу судить скажем популярная в питере секта "свидетелей Воеводского" действует скорее в этом роде - пытается переписать все так чтобы оно "автоматически доказалось"
Реальные же успехи были достигнуты на других путях:

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

- механизации рутинных операций - типа систем контроля версий etc

- и главное: выработкой методик как надо устраивать программы, чтобы они не теряли обозримость:
Наиболее важные тут видимо:
- структурное программирование
- абстракция данных и модульность с инкапсуляцией
- объектное программирование
- функциональное программирование (в котором с этой точки зрения главное - что отказ от изменяемых состояний радикально сокращает количество неявных зависимостей по данным - один из главных источников неуправляемости)

Ну и одновременно - развитие языковой поддержки всего этого - что тоже дает эффект.

Imho математики совершенно неизбежно придут к тому же - но пока как-то пытаются трясти, там где думать надо - и ища как автор статьи, аналоги в компутерщине - слона-то как раз и не видят - а ищут под соим фонарем
Subscribe

Recent Posts from This Journal

  • "Трагедия курьера"

    Что забавно - попытки партии и ментов усиливать контроль за всем на практике дают противоположный результат - паспорта у меня в данный момент нет,…

  • Из комментов

    Впрочем у истории с чёрными кораблями были две забавные концовки — одна в Порт-Артуре, другая — в Жемчужной гавани

  • Во всяком культивировании

    всяких покрытых богоматерей, дней оун-упа и прочих мининых-невских-пожарских и тп меня раздражают не поводы (на них мне действительно насрать) а…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 20 comments

Recent Posts from This Journal

  • "Трагедия курьера"

    Что забавно - попытки партии и ментов усиливать контроль за всем на практике дают противоположный результат - паспорта у меня в данный момент нет,…

  • Из комментов

    Впрочем у истории с чёрными кораблями были две забавные концовки — одна в Порт-Артуре, другая — в Жемчужной гавани

  • Во всяком культивировании

    всяких покрытых богоматерей, дней оун-упа и прочих мининых-невских-пожарских и тп меня раздражают не поводы (на них мне действительно насрать) а…