Языки программирования
Я тут понял удивительную вещь. Одно из тех открытий, когда вдруг понимаешь, что всю жизнь говорил прозой. Ну когда обнаруживаешь, что ты какую-то вещь считал естественной, считал что вообще все вокруг так думают, а оказывается, ровно наоборот: так не думает почти никто
( Read more... )
Comments 53
Все ТЗ на разработку языков программирования тоже написаны на естественном языке.
Отсюда версия - языки программирования вовсе не уникальная сущность для моделирования, а временное решение. До тех пор, пока с компьютером не станет возможным общаться на человеческом языке.
И отсюда вовсе не следует, что языки программирования отомрут. Они останутся ровно также, как в математических текстах остаются специфические обозначения, упрощающие и сокращающие изложение и делающие математический текст нечитабельным для большинства непрофессионалов.
Reply
https://youtu.be/Ct-lOOUqmyY
Reply
"Искусственный интеллект напишет бинарный код из полного и точного технического задания. Вы, кстати, знаете, как называется полное и точное тех. задание? Оно называется 'Программа'."
Для общения с машиной, которая делает 3*10^9 операций в секунду, то есть, может ошибиться 10^13 раз в час, техническое задание должно быть составлено без ошибок и недомолвок. А для этого нужны формальные языки.
Кстати, с людьми ровно то же самое - как правило, когда нужно точно описать алгоритм, используют псевдокод, а не естественный язык.
Reply
Можешь данную идею развернуть? Потому что на первый взгляд оно противоречит вот этому:
> и как этого избежать не теряя в элегантности описания построений
Ведь императивность как раз и мешает нам строить элегантные рассуждения про концепции в некоей программе?
> Математика кишмя кишит построениями, от и до.
Так-то да, но ведь далеко не всё сводится к конструктивной математике. Полным полно доказательств от противного например. Или я тебя как-то не так понял?
Reply
Это если понимать императивность в наивном смысле, т.е. “чтоп можно было написать как на С и работало”. Я вижу это совсем по-другому, а именно что в языке, основывающемся на MLTT, хорошо иметь поддержку кастомных модальностей, в том числе в смысле modal substructural logic. Такие модальности позволяют концептуально-честно описывать такие вещи как взаимодействие со внешним по отношению к программе миром, например с пользователем или внешними сервисами. И это же позволяет во фрагменте кода, где был включён import соответствующей модальности писать код очень похожий на императивный, только концептуально чище.
Наружу в purely functional этот фрагмент кода вкладывается путём, грубо говоря, обёртывания в ту монаду (модальности в простейшем случае описываются при помощи пары сопряженных монады и комонады, но я бы не хотел вдаваться в технические подробности).
Reply
Reply
https://jozefg.github.io/papers/2019-implementing-modal-dependent-type-theory.pdf
Reply
"Декларативная предметная область" это значитъ, что уже есть принятый и понятный людямъ языкъ, на которомъ люди объясняютъ другъ другу спецификацiи задачъ въ этой области, и этотъ языкъ однозначно и адекватно задаетъ и формулировку задачи, и ея рѣшенiе.
Два примѣра "декларативной предметной области":
1. Традицiонная запись ариѳметическихъ выраженiй. Мы пишемъ (x + y) / 2 + 1 и намъ сразу понятно, что и какъ будетъ вычислено. Когда придумали языкъ Фортранъ, гдѣ такiя выраженiя автоматически правильно компилируются, продуктивность программистовъ на порядокъ выросла. Не надо писать тесты, провѣряющiе, что мы правильно распредѣлили память или что второй знакъ "плюсъ" вычисляется послѣ дѣленiя. Мы ( ... )
Reply
Метод решения задачи выбирается компилятором. И в случае арифметических выражений мы точно знаем ключи компилятора, которые приведут к разным алгоритмам на современных x86 системах - это включение/выключение sse, avx и fp87.
Есть разные оптимизации, трансформирующие выражения 2*x в x << 1 или x + x при компиляции. Результат вычислений будет похожим на то, что подразумевалось. Но это, собственно, всё, что гарантируется.
Reply
Остаются только синтаксические идиосинкразии.
Reply
А если как инструменты для концептуализации и моделирования предметной области, то, разумеется, нет. В частности в некоторые из них вкладывается хотя бы интуиционистская логика первого порядка, а в некоторые только фига с маслом вкладывается.
Reply
Reply
Leave a comment