Новые перспективные языки - где они?

Тут вон недавно $7.5M выделили авторам небезызвестной HoTT, будут в том числе и реализацию своего языка делать.

*из криокамеры*
А где-то кто-то объяснял, зачем делать язык с HoTT? Да и вообще, при чем HoTT к инфоматике?

Rust же, ну. Go и M# тоже молоды.

А где-то кто-то объяснял, зачем делать язык с HoTT?

Чтобы можно было заимплементить как минимум всё то, что написано в их книге, очевидно же. Coq слишком ограничен.

Да и вообще, при чем HoTT к инфоматике?

Как теория типов относится к информатике? Лол. Почитай хотя бы введение что ли: http://hottheory.files.wordpress.com/2013/03/hott-a4-611-ga1a258c.pdf

Две чашечки чая этому адеквату.

В ближайшие 2 – 4 года ничего не изменится.

Julia?

Вон создали Rust - а пользователей я не видел.

Вот выйдет 1.0 — тогда можно будет говорить, что «создали». А пока нет.

Тут вон недавно $7.5M выделили авторам небезызвестной HoTT, будут в том числе и реализацию своего языка делать.

А какие у него киллер-фичи будут?

Meth? Смотрите на наркомана!

Вот пример, особое внимание стоит уделить первому абзацу, там ответ на твой вопрос http://homotopytypetheory.org/2011/03/26/higher-fundamental-groups-are-abelian/

А где-то кто-то объяснял, зачем делать язык с HoTT?

Как это «для чего»? Для получения лулзов, ессно! Вообще, вся современная математика (начиная с конца 19-го века) существует исключительно ради получения лулзов.

Для получения лулзов, ессно!

Да ладно, скорее для профита. Сидеть в теплом институтике и имитировать бурную деятельность, пописывая бесполезные каракули с умным видом, — вполне непыльная работенка. А если еще лицо по-умнее скривить, могут и вообще грант выдать. Лучше только чиновником.

Перефразирую - зачем они?

Новые перспективные языки - где они?

Ээээсперааанто!

Вспомнил песню Rammstein - Te Querto Puta.

Я даже знаю на нём ожно выражение «Ne mortigu min». Я читал Гарри Гаррисона

Разработчики Rust, скорее всего, вобьют последний гвоздь в гроб подходу «собралась кучка мудаков, почесала левую пятку и по её велению запилила очередное нинужно».

Причастность разработчиков Rust к этому подходу, как и ненужность самого языка, очень спорна.

В научной среде есть язык математики. Зачем им убогие ЯП?

поробуй

1. ввести в компьютер сложную формулу

2. распарсить её

3. вычислить (да, детка, если это интеграл, над его взять, а если бесконечный ряд — исследовать сходимость)

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

а после «закидывания» связь прервётся, да? Только радио?

А где-то кто-то объяснял, зачем делать язык с HoTT? Да и вообще, при чем HoTT к инфоматике?

простите мою серость, HoTT это чё? Гугл сказал: http://en.wikipedia.org/wiki/Sexual_appeal

Вообще, вся современная математика (начиная с конца 19-го века) существует исключительно ради получения лулзов.

а зачем Архимед площадь параболы вычислил?

Да ладно, скорее для профита. Сидеть в теплом институтике и имитировать бурную деятельность, пописывая бесполезные каракули с умным видом

к счастью, часто математики действительно полезные вещи придумывают. Увы, на 95% ты прав...

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

ну вот тебе например Эварист Галуа, который придумал поле своего имени

Если бы не он, сейчас бы ты сидел с FDD на 360Кбайт и с HDD на 10Mb весом 10кг, и ценой $1000.

Просто ты глупый, и думаешь, что прогресс двигают только технологии. Нет. Телега с кобылой останется телегой с кобылой. Технологии не сделают из телеги самолёт. За Over9000 лет — не сделали. Ещё математика нужна.

Конечно я не могу назвать великих математиков современности, но лишь потому, что их открытия _пока_ не нужны. Галуа тоже вот подстрелили в 20 лет, а на то, что он великий математик всем было насрать.

придумал поле своего имени

придумал

вся твоя популистская суть в одном слове.

То-то все математики так роскошуют. Иногда смотришь на такого - он и преподает, и работы в журналы постит, и то, и се - а озеро в черногории не покупает. Короче, ты неправ.

вся твоя популистская суть в одном слове.

блондинки вроде тебя иначе не понимают. Ты хоть начальную школу закончил?

Самолет создавался не математиками, а безымянными массами смельчаков, которые прыгали с возвышенностей, оборудованные разного рода хитроумными устройствами. А уж сколько было бесчисленных экспериментов в аэродинамических трубах, ты себе даже представить не можешь.

Но у таких даунов как ты все просто — боженька создал математиков, а математики создали самолет.

Создают ли новые ЯП? Что сейчас происходит в научной среде?

В науке со скоростью света распространяется питонячее УГ, а вы про уберновые крутые ЯП.

Конечно я не могу назвать великих математиков современности, но лишь потому, что их открытия _пока_ не нужны.

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

Чтобы можно было заимплементить как минимум всё то, что написано в их книге, очевидно же. Coq слишком ограничен.

В чём заключается ограниченность? Или так — номер формулы из книжки которая не переписывается на Coq или Agda прямо вот как есть?

HoTT это чё?

Homotopy type theory.

Но у таких даунов как ты все просто — боженька создал математиков, а математики создали самолет.

ох детка... Ну давай про самолёты не будем, твоя мама мне этого не простит.

Давай про флешки. Вот флешки изобрели 30 лет назад, но их ресурс до сих пор никакой: MTBF 1000 циклов примерно. Как же флешки работают, если даже файл размером 100Мб будет битым с гарантией 146%?

Очень просто, берём 1000 бит данных, и добавляем к ним 200 известных бит (например нулевых)

Проблема №1: как размешать 1200 бит?

Потом когда прочитаем, 1000 бит будет гарантированно целые, а ≥200 бит будут битыми.

Проблема №2: как узнать, какие биты битые, а какие целые?

Ну и наконец проблема №3: как восстановить изначальные 1000 бит из ≥1000 целых бит? Ведь целые биты это не изначальные, а продукт смешивания их из изначальных и известных?

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

Жду с нетерпением твоего решения, раз ты считаешь, что «математика не нужна».

Современная математика и математика времен Галуа — совершенно разные дисциплины. Поэтому я так и не понял, как пример с Галуа может что-либо говорить о дне сегодняшнем.

то, чем занимался Галуа, является фундаментом для современной техники.

Сегодняшними математиками наглядно доказывается, что можно создать целый мир, который не будет пересекаться с реалиями окружающей среды сколь угодно длительное время, в идеале, бесконечно большое.

и что? Те же поля Галуа в его время были никому нафиг не нужны. Он придумал числа, которым тупо нечего было считать. Т.е. совершенно бесполезную и никчёмную арифметику. И только в конце двадцатого века она ВНЕЗАПНО оказалось очень годной для кодирования информации в компьютерах для хранения и передачи.

та я уже нагуглил. Там след. строчка после «сексапильности». Тонко.

И только в конце двадцатого века она ВНЕЗАПНО оказалось очень годной для кодирования информации в компьютерах для хранения и передачи.

Можно пруф в качестве ликбеза?

Go. Но все перспективы в области практики лежат. Чисто инженерная штука.

Создают ли новые ЯП?

Нет, ибо AI на подходе, будете с ним как-то договариваться, возможно по-фене тоже можно будет.

ну вот безумно устаревшая статья Криса Касперки https://web.archive.org/web/20130918023033/http://www.insidepro.com/kk/027/02...

Только ты учти, что во первых прошло немало лет с момента написания, а во вторых, не знаю как сейчас, но в то время Крис сам толком не разобрался в теме (т.к. в итоге рекомендует ломать коммерческие библиотеки).

Но там есть ссылки на источники.

Нет, ибо AI на подходе

ты идиот? На каком «подходе»?

В чём заключается ограниченность? Или так — номер формулы из книжки которая не переписывается на Coq или Agda прямо вот как есть?

Если честно, я не очень хорошо разбираюсь, лишь где-то читал.

На самом деле сама книжка использует язык теории типов для выражения мыслей (U, Sigma, Pi, Id) — так что естественно, что разные вещи были реализованы на Coq и Agda по нескольку раз разными людьми. Взять, например, 8.1 про π₁(S¹) ≃ ℤ — на агде раз, два, три. Сравнить многабуков encode-decode proof (8.1.4) на две страницы и его реализацию:

{- 3. Dan’s encode-decode proof -}

-- This is quite similar to [paths-mike], we’re doing it by circle-induction,
-- the base case is [encode-loop^] and the loop case is using the fact that [ℤ]
-- is a set (and [loop^succ] is already used in [decode])
decode : (x : S¹) → (S¹Cover x → base == x)
decode =
  S¹-elim loop^ (↓-→-in (λ {n} q →
                 ↓-cst=idf-in
                   (loop^succ n ∙ ap loop^ (S¹Cover.↓-loop-out q))))

decode-encode : (x : S¹) (p : base == x) → decode x (encode p) == p
decode-encode _ p = J (λ x p → decode x (encode p) == p) idp p  -- Magic!

-- And we get the theorem
ΩS¹≃ℤ : (base == base) ≃ ℤ
ΩS¹≃ℤ = equiv encode (decode base) encode-loop^ (decode-encode base)

В том и проблема. Математика из скромной работящей служанки превратилась в жирную ленивую и капризную царицу.

Вот еще новый язык: http://lapis.at.ua/

Я джва года ждал такой язык.

On the computer science side, applications include using homotopy type theory’s more general notion of equality to make formal verification of software easier. On the mathematical side, applications include using type theoretic proof assistants, like Coq and Agda, to give formal, machine-verified, proofs of mathematical theorems.

Как бы проблема в том, что ни то ни другое на практике ненужно и неприменимо.

ну вот тебе например Эварист Галуа, который придумал поле своего имени

Он только описал конструкцию такого поля, ничего полезного он эти поля не сказал.

Смысл вклада Галуа в том, что он вообще создал современную математику в том виде, в каком она есть. А какие-то поля - это так, хуита.

Но у таких даунов как ты все просто — боженька создал математиков, а математики создали самолет.

Самолет создали, конечно, не математики, но без довольно сложного матаппарата сделать самолет, который будет нормально летать, а не планировать на пару сотен метров - малореально. Математика тут необходимое условие - хоть и недостаточное.

Ну ты не прав. Те же работы о решении у-й в радикалах, которыми в основном и занимался Галуа, тогда были полезны точно так же как и сейчас - никак. И делалось все так же ради лулзов, хоть и имело несколько другую форму, да.

Он придумал числа, которым тупо нечего было считать. Т.е. совершенно бесполезную и никчёмную арифметику.

Им и сейчас нечего считать. В том смысле, что элементы конечного поля в кодировании интерпретируются как символы (или их последовательности), а не как числа. Числами их никто не называет и не считает.