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

[akuklev]

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

Comments

[chaource]

До появленiя FP, въ трудѣ программиста не было мѣста для математическихъ концепцiй. Ни теорiя категорiй, ни теорiя логическихъ доказательствъ, ни теорiя типовъ, ни HoTT не были нужны, потому что они никакъ не облегчали трудъ программиста и даже вообще не относились къ процессу написанiя программъ. Если посмотрѣть на книгу Кнута "Искусство программированiя", то она заполнена угадыванiемъ того, какъ написать программу и потомъ доказательствомъ, что Кнуту удалось угадать правильно.

Только въ FP математика реально используется для построенiя языка программированiя и для написанiя программъ. Только въ FP построенiе языковъ и программъ можно формализовать достаточно содержательнымъ образомъ, чтобы программистъ могъ думать о программѣ въ терминахъ "здѣсь у меня коварiантный функторъ - здѣсь у меня естественное преобразованiе - значитъ, тутъ тоже долженъ быть коварiантный функторъ" и создавать кодъ, пользуясь этими концепцiями.

[akuklev]

Мне теперь в ЖЖ очень нехватает лайков. В данный момент, чтобы поставить их ко всём трём вашим комментариям.

[chaource]

По существу, вы выдвигаете слѣдующую гипотезу: если языкъ программированiя хорошо подходитъ для того, чтобы на немъ записать аксiоматику натуральныхъ чиселъ Пеано, универсальной алгебры, и т.п., то этотъ языкъ программированiя будетъ также хорошъ для написанiя базъ данныхъ, вебъ-браузеровъ и бизнесъ-приложенiй (т.к. языки программированiя въ реальномъ мiрѣ нужны только для этого).

Иными словами, дается рекомендацiя дѣлать такiе языки программированiя, для которыхъ предметная область разнообразныхъ индуктивныхъ алгебраическихъ конструкцiй является "декларативной предметной областью", т.е. чтобы на данномъ языкѣ было легко и просто записать аксiоматику Пеано или аксiомы категорiи или другiя такiя вещи.

Неочевидно, что эта гипотеза вѣрна. Пока что, напримѣръ, неочевидно, что Coq, Agda и Idris существенно облегчаютъ программированiе по сравненiю съ OCaml и Haskell.

[akuklev]

> По существу, вы выдвигаете слѣдующую гипотезу: [...]

Не совсем; я считаю, что языки программирования в идеале должны в том числе подходить и для этого. Я нигде не утверждаю, что этого достаточно для декларативного описания других предметных областей. Пример языка Coq отлично иллюстрирует эту мысль - в этом языке напрочь отсутствует машинерия для концептуализации чего бы то ни было, выходящего за пределы конструктивной математики. (В Idris 2 это уже не так.)

[ext_3948950]

> Ну как можно _хотеть_ работать на языке, на котором _невозможно сказать то, что ты имеешь в виду_?

Как всегда - мы хотим максимальной свободы для СЕБЯ, но минимальной - для соседа. Или для себя же трёхмесячной давности, когда приходится свои же бредни разгребать...

[66george]

А посмотрите, что я напрограммировал
https://mega.nz/file/igo0zDBC#JgIYMtie3UmKXgDgtWBKzXE25xPA-qvZuKMKQ3y8fFk

[akuklev]

Эге! Осталось только придумать, где мне взять виндоус, чтобы это запустить :)

[66george]

Поставьте Qt и попробуйте собрать под Linux (есть шанс, что заработает, хотя я не отлаживал под Linux)

[38irtimd]

> Но если бы это было так, не было бы затруднений несколькими умелыми штрихами превращать словесные описания в формализованные машинно-читаемые. Раз это далеко не так, значит в словесных описаниях лишь видимость conceputal clarity, а на самом деле что-то существенное замели под ковёр.

это в общем ниоткуда не следует.

практика показывает, что под ковёр заметается как раз что-то занудное. насколько я понимаю, это как раз и есть челлендж всех этих новомодных систем доказательств --- сделать так, чтобы не писать то, что в текущей практике не принято прописывать. именно поэтому так мало доказательств на этих языках. последнее, что я слышал --- какой-то кусок про этальные когомологии кодифицировали. даже не помню, в чём (idris что ли). ну ок, математика 50летней давности.

[66george]

Мне кажется, я нашёл баг в Факторе. Посмотрите, пожалуйста
https://www.blogger.com/comment.g?blogID=8513438391157777465&postID=8680112867593321902