amarao (amarao_san) wrote,
amarao
amarao_san

Category:

программирование - это такая неряшливая математика

Вот вам интересная мысль.

Что такое бит? Существует ли он?

Программирование (как математика) начинается с допущений:

"Предположим, существует бит, который может принимать значение "истина" и "ноль" и набор операций, применяемых к битам (NOT OR AND ETC)..."

А дальше там чистой воды математика, которая перестаёт думать о реальном мире и зарывается в абстракции, построенные из этих допущений.

В реальный мир программирование вываливается ровно в тот момент, когда приходит инженер и говорит "о, я вот тут из транзисторов и палок скрутил фигулину, которая в первом приближении ведёт себя как этот твой NOT, и можно считать, с некоторыми допущениями, что 0.1В - это ложь, а 0.8В - истина". (по поводу первого приближения: https://en.wikipedia.org/wiki/Latch-up)

Дальше эта абстрактная штука (программирование) периодически вываливается в набор допущений (если я запишу в порт 0x12 значение 0x42, то лампочка зажжётся), которое наиболее грустные из программистов называют "монада IO". Но в местах, которые не касаются этих допущений, мы имеем чистую математику.

Давайте назовём этот объект "TestEnv", и он будет обладать свойством get, которое по имени аргумента возвращает значение или рейзит эксепшен... (и поехало дальше всё это).

Главным, фундаментальным различием этой математики от математики на бумажке является то, что эти логические утверждения никто не проверяет. До определённой степени это может делать интерпретатор/компилятор (например, сказав, что утверждение о том, что TestEnv принимает только имя аргумента и утверждение о том, что TestEnv(arg_name, default_value=None) противоречивы), на каком-то уровне runtime, но финальное утверждение, что данный набор утверждений, лемм, тезисов и т.д. является истинным (то есть решает заданную задачу) совершенно никем не проверенное, и осложняющееся тем, что каждый наш запуск проверяет только частный случай.

Но я не о математическом доказательстве правильности программ. Я о другом. Поскольку программирование - это чистая математика, то все объекты программирования существуют ровно настолько, насколько существуют любые другие математические объекты. Например, совершенно равноправен gevent со своим monkeypatching'ом и, допустим, частичная сумма ряда. Или цепная дробь. Или даже всеми любимый треугольник.

И в тот момент, когда программист решает назвать тип данных или класс в коде 'realm', в этот момент у нас появляется realm, и он настолько же реален, насколько реальна идея о детерминанте матрицы.

Но тут же начинают наблюдаться и различия: детерминант матрицы - хорошо изученная штука, и о его смысле и свойствах согласны все. А realm может оказаться самопротиворечивой конструкцией (например, утверждать, что имеет метод .doit, но вызывать внутри __init__'а метод self.do_it).

Математик, изредка придумывая новое слово (сущность, объект), вкладывает в него очень мало свойств и тщательно их изучает. Программист придумывает новые слова, сущности и объекты едва ли не со скоростью печати. Его свойства очерчиваются крайне небрежно и в минимальном объёме (и целые пласты работы программистов посвящены тому, как это делать побыстрее да похалтурнее), они практически не изучаются, и тут начинают громоздиться новые объекты и свойства. Более того, математические объекты обычно являются универсальными и добавляются в глобальный namespace человечества, а программист, за редкими исключениями низкоуровневых библиотек, большую часть своих объектов прячет глубоко в приватном namspace'е, даже если от них зависят какие-то глобальные сущности, класса "цифровой подписи".

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

И у меня есть какое-то странное ощущение, что никто не исследовал эту идею с подобной позиции. Можем ли мы иметь противоречивую и неполную систему утверждений, в которой есть заведомо ошибочные выводы, но которую мы продолжаем применять для практических надобностей?
Tags: programming
Subscribe

  • systemd-networkd, netlink и arp флуд

    Нереально странный баг пофикшен с помощью eBPF затычки. Для меня большой неожиданностью является реакция на него.…

  • Rust soundness

    Каждый раз, когда я сталкиваюсь с маленькими "но" в Rust'е, это ощущение тщательной продуманности. Например, простейшие fold-функции для итераторов:…

  • still_ntp

    В ходе локального мозгового штурма у меня родилась суперидея. Надо написать ntp сервер, который может отдавать указанную дату. Т.е. сказали при…

  • Post a new comment

    Error

    default userpic

    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.
  • 19 comments

  • systemd-networkd, netlink и arp флуд

    Нереально странный баг пофикшен с помощью eBPF затычки. Для меня большой неожиданностью является реакция на него.…

  • Rust soundness

    Каждый раз, когда я сталкиваюсь с маленькими "но" в Rust'е, это ощущение тщательной продуманности. Например, простейшие fold-функции для итераторов:…

  • still_ntp

    В ходе локального мозгового штурма у меня родилась суперидея. Надо написать ntp сервер, который может отдавать указанную дату. Т.е. сказали при…