В нескольких комментариях упомянута несовместимость из-за реализаций только любимых расширений авторов; как раз чтобы получить небольшой набор важных и общих расширений, есть XMPP Compliance Suites (см. XEP-0387).
Но в то же время не все популярные клиенты поддерживают их, и не все популярные серверы поддерживают их по умолчанию. С библиотеками тоже не всё хорошо, в большинстве случаев клиенты и серверы реализуют XMPP с расширениями заново.
Пропустил вопрос про натравливание на существующий код: нет, это отдельный язык, так что если хочется «натравить» — нужно сформулировать язык-цель на этом языке, т.е. построить целую модель, причём сложную, и потом уже анализировать. Это не слишком практично, а также долго и сложно.
С описаниями протоколов или структур может быть практичнее, но, думаю, тут проще будет говорить о конкретных примерах (протоколов/структур и желаемых доказательств) — они могут быть довольно разными.
По поводу верификации — есть два основных подхода: первый — постановка и доказательство теорем после написания самой программы, второй — упор на точность спецификации. Программы в обоих случаях должны быть написаны либо на этом языке, либо на языке, интерпретатор которого на нём написан (что сильно усложняет задачу, но иногда бывает полезно). Но, в то же время, верифицировать можно не только программы, но и любые системы, которые мы можем смоделировать — тогда верификация заключается в доказательстве наличия интересующих нас свойств.
Внедрить для реализации критичных участков, по крайней мере в теории, вполне реально: поскольку идёт компиляция в те же C и JS, ничто не мешает вызывать получившиеся функции из этих языков. Но в Idris на данный момент это не приоритет, так что на практике это будет неудобно.
Штуки наподобие SSL, опять-таки в теории, ничто не мешает реализовать; на практике же, как упомянул в статье, язык «необкатан», и прямо сейчас можно стать первооткрывателем багов компилятора. Но цель разработчиков — сделать его пригодным для таких задач.
Синтаксис не так уж строго взят из Haskell: в том же Haskell они поменяны местами, если сравнивать с ML. В Agda тоже используется одно двоеточие для типов и два для списков, что многим представляется более удобным.
Но проблема замечена верно: уже не раз у меня возникали проблемы с двоеточиями при чередовании Agda/Idris с Haskell.
Но в то же время не все популярные клиенты поддерживают их, и не все популярные серверы поддерживают их по умолчанию. С библиотеками тоже не всё хорошо, в большинстве случаев клиенты и серверы реализуют XMPP с расширениями заново.
С описаниями протоколов или структур может быть практичнее, но, думаю, тут проще будет говорить о конкретных примерах (протоколов/структур и желаемых доказательств) — они могут быть довольно разными.
Внедрить для реализации критичных участков, по крайней мере в теории, вполне реально: поскольку идёт компиляция в те же C и JS, ничто не мешает вызывать получившиеся функции из этих языков. Но в Idris на данный момент это не приоритет, так что на практике это будет неудобно.
Штуки наподобие SSL, опять-таки в теории, ничто не мешает реализовать; на практике же, как упомянул в статье, язык «необкатан», и прямо сейчас можно стать первооткрывателем багов компилятора. Но цель разработчиков — сделать его пригодным для таких задач.
Но проблема замечена верно: уже не раз у меня возникали проблемы с двоеточиями при чередовании Agda/Idris с Haskell.