Есть ли доказуемые языки реального мира? (Scala?) - PullRequest
50 голосов
/ 31 октября 2010

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

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

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

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

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

Ответы [ 11 ]

2 голосов
/ 27 января 2015

Как насчет Идрис и Агда ? Достаточно ли реального мира?

В качестве хорошего примера из реальной жизни есть проект, целью которого является предоставление проверенной библиотеки HTTP REST, написанной в Agda, под названием Lemmachine: https://github.com/larrytheliquid/Lemmachine

...