Обновить

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

Язык очень молодой, сообществу нужны программисты, а не только математики, чтобы сделать язык готовым к промышленному применению. Сейчас очень не хватает многих прикладных библиотек. Язык то вышел в этом десятилетии! Причём многие из этих библиотек - низко висящие фрукты - их довольно легко написать!

Скажите, о чём бы вы хотели прочитать в моей будущей статье? Какие аспекты вам наиболее интересны? Решение какого-нибудь примера? Или просто обзор языка и его экосистемы? Может быть, рассказ о том, как для написания доказательств используют искусственный интеллект?

Предлагайте свои варианты и задавайте вопросы.

Теги:
Всего голосов 5: ↑5 и ↓0+7
Комментарии4

Метод Каллана: я повторял предложения три года

Как курс английского, построенный на повторении, оказался самым полезным, что я изучал, — и почему любой разработчик за пределами англоязычного мира рано или поздно сталкивается с тем же выбором.

Фото: little Gabriel, Unsplash

Мне было четырнадцать, когда я решил, что школа не научит меня английскому.

Шёл 2009 год. Я учил немецкий и не любил его — не сам язык, а тот факт, что его выбрали за меня. К тому времени я уже писал первые строки кода и заметил вещь, которая казалась мне очевидной и, судя по всему, никому вокруг: любой язык программирования, который я хотел выучить, был документирован на английском. Любой ответ на форуме. Любое сообщение об ошибке. Любая книга, которую стоило читать.

Так что я попросил записать меня куда-нибудь всерьёз. Так я оказался в Британский Центр в Тбилиси, в двухэтажном здании на улице Пекини, в комнате с одиннадцатью другими людьми и преподавателем, который говорил быстрее, чем я успевал думать.

Метод Каллана: я повторял предложения три года

Публикации