Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Языки программирования

Я тут понял удивительную вещь. Одно из тех открытий, когда вдруг понимаешь, что всю жизнь говорил прозой. Ну когда обнаруживаешь, что ты какую-то вещь считал естественной, считал что вообще все вокруг так думают, а оказывается, ровно наоборот: так не думает почти никто.

Итак, открытие: кажется, подавляющее большинство математиков и подавляющее большинство программистов думаю о языках программирования как об инструментах для “компьютерщиков”. Ну типа как какие-то там специальные отвертки с моторчиком или вроде того, чтобы где-то покрутить и компьютер начал делать то что нужно.

Для меня язык программирования это, разумеется, инструмент концептуализации и моделирования той или иной предметной области. В первую очередь математических построений, потому что любая другая предметная область пользуется математическими конструкциями (попробуйте сформулировать какую-нибудь бизнес-логику, не прибегая к понятиям пары, списка и числа). Естественно sine qua non для языка программирования в моей голове — возможность записывать на нём концептуально чисто и элегантно известные уже 2300 лет геометрические построения и алгоритм Эвклида.

Именно поэтому я столько лет не понимал, когда очень сильные программисты начинали тирады что в языках программирования не нужна поддержка замыканий и прочего FP, или наоборот ратовали только за pure FP без каких-либо выразительных средств для описания императивных алгоритмов. Ну как можно _хотеть_ работать на языке, на котором _невозможно сказать то, что ты имеешь в виду_? Как можно хотеть разговаривать на птичьем языке Эллочки-людоедки, в рамки которого просто не влезают _правильные_ концептуализации того, с чем мы работаем?

Именно поэтому я столько лет не понимал, когда знакомые математики отмахивались от HoTT со словами “ну, наверное программистам это полезно, но зачем это нужно в математике пока непонятно”. Как это может быть непонятно? Математика кишмя кишит построениями, от и до. Определение какиех-нибудь когомологий это описание того, как их строить. Теорема о неявной функции — это декларативное описание того, как строить функцию по её уравнению.

Мы можем конечно делать вид, что словесное описание с картинками (коим пользовался и Эвклид ещё ~2300 лет назад), это и есть идеальный способ описания построений. Но если бы это было так, не было бы затруднений несколькими умелыми штрихами превращать словесные описания в формализованные машинно-читаемые. Раз это далеко не так, значит в словесных описаниях лишь видимость conceputal clarity, а на самом деле что-то существенное замели под ковёр. Значит должно быть интересно, что именно замели под ковёр, и как этого избежать не теряя в элегантности описания построений. И тут природа как обычно даёт нам подсказку, что мы копаем в нужном месте — тем удивительным фактом, что на пути формализации построений откуда ни возьмись вдруг возникает нетривиальная современная математика.
Subscribe

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 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.
  • 53 comments
Previous
← Ctrl ← Alt
Next
Ctrl → Alt →
Previous
← Ctrl ← Alt
Next
Ctrl → Alt →

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…