Namdak Tonpa (maxim) wrote,
Namdak Tonpa
maxim

Языки и Программирование: Coq

Почему Coq не был офигенным еще 5 лет назад? Потому что никто не преуспел на его основе сделать язык общего назначения. Поискав "coq as general purpose language" вы пока ничего не найдете. На Coq дофига пакетов в OCaml, но большинство из них математические модели.
Но не на количество моделей надо смотреть, а можно ли на нем писать действительно что-то мощное, ну ладно мощное, хотябы хелоу ворлд и ехо сервер :-) 3 года назад Гиюм Кларе сделал веб-сервер Pluto, и если вы посмотрите на исходники, то найдете стиль poor man человека, с простенькими эфектами, простенькой функциональностью — но все работает. Я хотел прорекламировать сайт автора, но он почему-то лежит, поэтому я просто тут расскажу на пальцах.

Как только появится возможно писать нормальные хелоу ворлды и кто-то возьмется за базовую рантайм библиотеку, которая по производительности была бы хотя бы на уровне PHP, тогда можно выходить в продакшин местячково начинать, ну как мы с n2o. Но кто будет писать на зависимых типах n2o.coq спросите вы? Ну Haskell тоже все боялись, а сейчас каждый джаваскриптер видел уже PureScript и Elm и может на них писать. Так, что мое мнение такое, как только найдется чувак который сделает приятную писанину на Coq сразу появится говнокод и продакшин. Тем более, что для рантайм библиотеки хватит и System F. Я вижу, что Coq мне приятней чем Scala/Haskell, и что его можно окультурить, есть Notation, можно даже DSL строить прямо в языке.

Кстати про OCaml, он тоже довольно омолодился за последние 5 лет. Во-первых opam, во вторых более нормальный сайт, Multi-core OCaml, самый быстрый паттерн мачинг, ReasonML тоже. Кароче куча всего, Lwt по сути уже стандарт де факто, успех Джейн Стрит и т.д. Неспешный но прекрасный язык для командной разработки. В ЖЖ дофига чуваков пишут/писали на OCaml.

Я к чему веду, так как мы с вами 10 лет назад интересовались лямбдой, 5 лет назад зависимыми типами, так и сейчас это кто-то делает, и этого будет больше. Конечно сама теория зависимых типов создает некую элитарность, но успех таких чистых и приятных штук как PureScript говорит, что даже сложные вещи можно сделать простыми, для меня лично PureScript — это реинкарнация Miranda, т.е. System F язык каким он должен быть. Такой же реинкарнацией Coq является Lean, а позже и EXE. Но Coq in Coq круче будет чем EXE in Rust, к примеру.

Я думаю, что нужно продолжать дело coq.io, и искать новые рабочие формы в библиотеке рантайм типов (а не PhD хелоу ворлды, которые если чесно уже заебали, буду стараться сделать не очередной хелоу ворлд!). Эту библиотеку, как я ее видел для EXE, можно написать на Coq и попробовать на простеньких догфуд программах, ну а что мы пишем, WebSocket, бинарный стриминг и очередя. Так, что вцелом, мы в Coq вас не тащим, но сами стараемся туда попасть раньше чем вы.
Tags: coq, cs
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

  • 13 comments