Существуют ли какие-либо доказуемые языки реального мира? (scala?)

меня учили формальным системам в университете, но я был разочарован тем, что они не казались используется в настоящем слове.

Мне нравится идея знать, что некоторый код (объект, функция, что угодно) работает, не путем тестирования, а с помощью доказательства .

Я Конечно, все мы знакомы с несуществующими параллелями между физической инженерией и разработкой программного обеспечения (сталь ведет себя предсказуемо, программное обеспечение может делать что угодно - кто знает! ), и мне бы хотелось узнать, есть ли какие-нибудь языки, которые можно использовать в реальном слове (слишком много просят о веб-фреймворке?)

Я слышал интересные вещи о тестируемости функциональных языков, таких как scala.

Как разработчики программного обеспечения какие варианты у нас есть?