Три языка

lex_kravetski — 26.03.2025 Когда в какой-то момент понимаешь, как всё сделано в языке Scala, то вдруг оказывается, что те места, где ты раньше терпеливо писал огромные бюрократические телеги, можно было бы описать так, как ты про них думаешь. При этом будучи одновременно точнее и абстрактнее в своём описании. Вроде как управлять мирозданием не так-то уж и сложно — это кто-то до того специально всё запутывал. Ощущается так, будто бы до того ты писал ручкой по бумажке и так же считал, а тут тебе вдруг сразу выдали Ворд с калькулятором. Это язык практического удобства, к чему, впрочем, сейчас движутся практически все мэйнстримные языки.

Когда в какой-то момент понимаешь, как всё сделано в языке Wolfram, то появляется ощущение, что мир в своей базе может оказаться совсем не таким, как тебе казалось с детства. Вроде бы было примерно понятно, как в компе что делается, языки это до какой-то степени отображают, тогда как математика всё это описывает через какие-то свои странные абстракции, но каким-то чудом всё сходится. Однако Wolfram показывает, что может быть совсем другое описание — единое в своей базе что для того, что для этого, но совсем не такое как давно уже было привычно. Ощущается так, будто бы вдруг оказалось, что вся наука — это фигня какая-то, а вот магия реально работает и всё объясняет. Это язык создания сложных правил на базе очень небольшого набора простых правил, но не тех, про которые ты привык думать, как про основу мышления.

Когда в какой-то момент понимаешь, как всё сделано в языке Lean, то появляется чувство, что весь мир правда можно описать как набор правил, но правилами ещё и можно проверить правила. Правила описывают очень прочные конструкции, которыми как-то подозрительно свободно охватываются огромные множества объектов. Это всё как бы логика, но почему-то запросто описывающая динамические процессы. Если Wolfram наглядно показывает, что всё на самом деле является строками, то Lean — что всё является практически всем. Нет особой разницы, строка это, число, выражение, функция, тип или состояние окружающего мира — в конечном счёте ты всё это можешь описать примерно одним и тем же способом. Ощущается так, будто ты наконец-то встретил универсальный язык рассуждений, в котором, к тому же, рассуждения существуют в связке с действиями, а потому доказанное суждение это не просто высказывание, а ещё и код, которым можно сделать что-то полезное. Это тоже язык создания правил на базе простых правил, но без ощущения того, что новые правила сложнее старых. Оно похоже на математику и классическую логику, но…

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

Оставить комментарий

Популярные посты:

• Ранее
• Архив