Недавно занялся изучением языка ATS — Applied Type System, который еще давно привлек мое внимание очень хорошими скоростными показателями на language shootout. Тогда меня отпугнула многословность решений, а оказывается она там не просто так: ATS содержит систему зависимых типов и конструктивных доказательств, которые поднимают уровень обеспечения коррекности до невиданных высот, вплоть до полного статического доказательства того, что программа делает то, что надо, и не содержит багов. Компилируется язык путем трансляции в Си и использования gcc, что дает ему очень простой FFI и все gcc-шные наработки по оптимизациям. А возможность указания массы условий и инвариантов в типах и их статического доказательства позволяет избежать лишних проверок в рантайме и обеспечить высокую скорость. В языке есть поддержка сборки мусора, но доступно также и подмножество языка, работающее без GC: можно собирать программы без GC, причем корректность работы с памятью обеспечивается системой типов. Документация по языку сильно разрозненная и неполная, но я начал серию постов по-русски с рассказами о фичах ATS доступным языком.

Введение в ATS и зависимые типы:
http://thedeemon.livejournal.com/41035.html

Другие посты:
http://thedeemon.livejournal.com/tag/ats