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

  • мы их теряем!

    Make: 1976 Прямо сейчас выходят на пенсию люди, для которых make был новомодной технологией, которую притащили хипстеры.

  • Админская мудрость

    Когда вывод strace на башовый скрипт становится понятнее самого скрипта, граница разумности давно пройдена.

  • Rules of internet

    Rule 34. There is porn of it. Rule 35. It's used to mine cryptocurrencies.

  • 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

  • мы их теряем!

    Make: 1976 Прямо сейчас выходят на пенсию люди, для которых make был новомодной технологией, которую притащили хипстеры.

  • Админская мудрость

    Когда вывод strace на башовый скрипт становится понятнее самого скрипта, граница разумности давно пройдена.

  • Rules of internet

    Rule 34. There is porn of it. Rule 35. It's used to mine cryptocurrencies.