Существуют ли доказуемые языки реального мира? (Scala?)
Меня учили формальным системам в университете, но я был разочарован тем, что они, казалось, не использовались в реальном слове.
Мне нравится идея быть в состоянии знать, что некоторый код (объект, функция, что угодно) работает, не путем тестирования, но с помощью доказательства.
Я уверен, что мы все знакомы с параллелями, которые не существуют между физической разработкой и разработкой программного обеспечения (сталь ведет себя предсказуемо, программное обеспечение может делать все что угодно - кто знает!), И я хотел бы знать, существуют ли какие-либо языки, которые можно использовать в реальном слове (слишком много, чтобы спросить о веб-фреймворке?)
Я слышал интересные вещи о тестируемости функциональных языков, таких как scala.
Как разработчики программного обеспечения, какие варианты у нас есть?
11 ответов
Да, есть языки, предназначенные для написания правильного программного обеспечения. Некоторые даже используются в промышленности. Искра Ада, пожалуй, самый яркий пример. Я разговаривал с несколькими людьми из Praxis Critical Systems Limited, которые использовали его для кода, работающего на Boings (для мониторинга двигателя), и это кажется довольно хорошим. (Вот отличное резюме / описание языка.) Этот язык и сопровождающая система доказательства используют второй метод, описанный ниже. Он даже не поддерживает динамическое выделение памяти!
У меня сложилось впечатление, что есть два метода написания правильного программного обеспечения:
Метод 1: Напишите программное обеспечение на удобном для вас языке (например, C, C++ или Java). Возьмите формальную спецификацию такого языка и докажите, что ваша программа верна.
Если ваши амбиции должны быть на 100% правильными (что чаще всего требуется в автомобильной / аэрокосмической промышленности), вы бы потратили немного времени на программирование и больше времени на доказательство.
Метод 2: Напишите программное обеспечение на немного более неуклюжем языке (например, в некотором подмножестве Ada или измененной версии OCaml) и напишите доказательство правильности. Здесь программирование и доказательство идут рука об руку. Программирование в Coq даже полностью приравнивает их! (Смотрите переписку Карри-Ховарда)
В этих сценариях вы всегда получите правильную программу. (Ошибка будет гарантированно укоренена в спецификации.) Скорее всего, вы потратите больше времени на программирование, но, с другой стороны, вы докажете, что это правильно.
Обратите внимание, что оба подхода зависят от того, что у вас под рукой есть формальная спецификация (как еще вы скажете, что такое правильное / неправильное поведение), и от формально определенной семантики языка (как еще вы сможете сказать, что такое реальное поведение)? вашей программы есть).
Вот еще несколько примеров формальных подходов. Если это "в реальном мире" или нет, зависит от того, кого вы спрашиваете:-)
- Доказательство теоремы Coq: программирование с помощью Coq (метод 2)
- ESC / Java (метод 1, хотя ни звук, ни полный)
- SpeC# (техника 1, ни звук, ни полный, хотя)
- Почему / Кракатау (техника 2, основанная на Java)
Я знаю только один "достоверно корректный" язык веб-приложений: UR. Ur-программа, которая "проходит через компилятор", гарантированно не будет:
- Страдают от любых видов атак с использованием кода
- Вернуть неверный HTML
- Содержат мертвые ссылки внутри приложения
- Несоответствия между формами HTML и полями, ожидаемыми их обработчиками
- Включите код на стороне клиента, который делает неверные предположения о службах стиля "AJAX", которые предоставляет удаленный веб-сервер
- Попытка неверных запросов SQL
- Использование неправильного маршалинга или демаршалинга при взаимодействии с базами данных SQL или между браузерами и веб-серверами
Чтобы ответить на этот вопрос, вам действительно нужно определить, что вы подразумеваете под "доказуемым". Как указывал Рики, любой язык с системой типов - это язык со встроенной системой доказательства, которая запускается каждый раз, когда вы компилируете свою программу. Эти системы доказательств почти всегда печально бессильны - отвечают на такие вопросы, как String против Int и избегая вопросов типа "список отсортирован?" - но они являются системами доказательства тем не менее.
К сожалению, чем сложнее ваши цели доказательств, тем сложнее работать с системой, которая может проверять ваши доказательства. Это довольно быстро перерастает в неразрешимость, если учесть огромный размер класса проблем, которые неразрешимы на машинах Тьюринга. Конечно, теоретически вы можете делать основные вещи, такие как доказательство правильности вашего алгоритма сортировки, но все, что угодно, будет идти по очень тонкому льду.
Даже для того, чтобы доказать что-то простое, например, правильность алгоритма сортировки, требуется сравнительно сложная система доказательств. (примечание: поскольку мы уже установили, что системы типов являются системой доказательств, встроенной в язык, я собираюсь поговорить о вещах в терминах теории типов, а не махать руками еще более энергично) Я вполне уверен, что для полной корректности сортировки списка потребуется некоторая форма зависимых типов, в противном случае у вас нет возможности ссылаться на относительные значения на уровне типа. Это немедленно начинает распадаться на сферы теории типов, которые оказались неразрешимыми. Таким образом, хотя вы можете быть в состоянии доказать правильность алгоритма сортировки списка, единственный способ сделать это - использовать систему, которая также позволит вам выдвигать доказательства, которые он не может проверить. Лично меня это очень смущает.
Есть также аспект простоты использования, о котором я упоминал ранее. Чем сложнее ваша система типов, тем менее приятной она будет. Это не жесткое и быстрое правило, но я думаю, что оно справедливо по большей части. И, как и в любой формальной системе, вы часто обнаруживаете, что выражение доказательства является более трудоемким (и более подверженным ошибкам), чем создание реализации в первую очередь.
Несмотря на все это, стоит отметить, что система типов Scala (например, Haskell) является Turing Complete, что означает, что вы можете теоретически использовать ее для доказательства любого разрешимого свойства вашего кода, при условии, что вы написали свой код в такой форме. Таким образом, он поддается таким доказательствам. Haskell почти наверняка является лучшим языком для этого, чем Java (поскольку программирование на уровне типов в Haskell похоже на Prolog, в то время как программирование на уровне типов в Scala больше похоже на SML). Я не советую вам использовать системы типов Scala или Haskell таким образом (формальные доказательства алгоритмической корректности), но эта опция теоретически доступна.
В целом, я думаю, что причина того, что вы не видели формальных систем в "реальном мире", проистекает из того факта, что формальные системы доказательств уступили беспощадной тирании прагматизма. Как я уже упоминал, создание ваших корректных доказательств требует столько усилий, что это почти никогда не стоит. Промышленность давно решила, что создавать специальные тесты было проще, чем проходить аналитические формальные рассуждения.
Вы задаете вопрос, который многие из нас задавали на протяжении многих лет. Я не знаю, что у меня есть хороший ответ, но вот несколько штук:
Есть хорошо понятые языки с возможностью быть проверенными в использовании сегодня; Lisp через ACL2 один, и, конечно, у Scheme также есть хорошо понятное формальное определение.
ряд систем пытались использовать чисто функциональные языки или почти чистые, такие как Haskell. В Хаскеле довольно много формальных методов работы.
На протяжении 20 с лишним лет существовала недолгая вещь для использования ручного доказательства формального языка, который затем был строго переведен на скомпилированный язык. Некоторыми примерами были IBM Cleanroom, ACL, Gypsy и Rose из Computational Logic, работа Джона МакХью и моей работы над надежной компиляцией C, а также моя собственная работа над защитой от руки для программирования на C-системах. Все они привлекли некоторое внимание, но никто из них не сделал это на практике.
Я думаю, что интересный вопрос: каковы будут достаточные условия для применения формальных подходов на практике? Я хотел бы услышать некоторые предложения.
Типизированные языки доказывают отсутствие определенных категорий вины. Чем более продвинута система типов, тем больше недостатков они могут доказать.
Чтобы доказать, что вся программа работает, да, вы выходите за пределы обычных языков, где математика и программирование встречаются, пожимают друг другу руки, а затем переходите к разговору, используя греческие символы, о том, как программисты не могут обрабатывать греческие символы. Это все равно о Σ этого.
Вы можете исследовать чисто функциональные языки, такие как Haskell, которые используются, когда одним из ваших требований является доказуемость.
Это интересно читать, если вам интересны функциональные языки программирования и чисто функциональные языки программирования.
Использование таких доказуемых языков в реальном мире было бы невероятно трудным для написания и понимания загадок. деловому миру нужно быстрое программное обеспечение.
"доказуемые" языки просто не масштабируются для написания / чтения кодовой базы большого проекта и, похоже, работают только в небольших и изолированных случаях использования.
Я участвую в двух доказуемых языках. Первый - это язык, поддерживаемый Perfect Developer, системой для определения sotfware, его доработки и генерации кода. Он использовался для некоторых больших систем, включая сам PD, и преподавался во многих университетах. Вторым доказуемым языком, с которым я работаю, является доказуемое подмножество MISRA-C, подробнее см. Блог проверки C/C++.
Мой (спорно) определение "реального мира" в контексте доказуемо-правильного кода:
- Это должно включать некоторую степень автоматизации, иначе вы будете тратить слишком много времени на проверку и обработку беспорядочных мелких деталей, и это будет совершенно непрактично (за исключением, может быть, программного обеспечения для управления космическими аппаратами и тому подобного, для чего вы может на самом деле захочется потратить мегабакс на тщательные проверки).
- Он должен поддерживать некоторую степень функционального программирования, которая помогает вам писать код, который является очень модульным, многоразовым и более легким для рассуждения. Очевидно, что функциональное программирование не требуется для написания или проверки Hello World или множества простых программ, но в определенный момент функциональное программирование становится очень полезным.
- Хотя вы не обязательно должны иметь возможность писать свой код на основном языке программирования, в качестве альтернативы, вы должны по крайней мере уметь машинно переводить код в достаточно эффективный код, написанный на основном языке программирования, на надежном путь.
Выше приведены относительно более универсальные требования. Другие, такие как способность моделировать императивный код или способность доказать правильность функций высшего порядка, могут быть важными или существенными для некоторых задач, но не для всех.
Ввиду этих моментов, многие из инструментов, перечисленных в моем блоге, могут быть полезны - хотя они почти все либо новы и экспериментальны, либо незнакомы подавляющему большинству отраслевых программистов. Там есть несколько очень зрелых инструментов.
Скала предназначена для того, чтобы быть "реальным миром", поэтому не было сделано никаких усилий, чтобы сделать его доказуемым. В Scala вы можете создавать функциональный код. Функциональный код гораздо проще тестировать, что, по-моему, является хорошим компромиссом между "реальным миром" и доказуемостью.
РЕДАКТИРОВАТЬ ===== Убрал мои неверные представления о том, что ML "доказуемо".
Как насчет Идриса и Агды? Достаточно ли реального мира?
В качестве хорошего примера из реальной жизни есть проект, целью которого является предоставление проверенной библиотеки HTTP REST, написанной в Agda, под названием Lemmachine: https://github.com/larrytheliquid/Lemmachine