Без заголовка

Всякие Charity, Epigram, Coq, Agda, Idris... Когда серьезно берутся в типах выражать логические утверждения, и делают там вычисления, эти вычисления обязаны гарантировано завершаться (см. также Total Functional Programming), в противном случае незавершающееся вычисление может служить доказательством чего угодно; а значит их язык не должен быть полным по Тьюрингу.