Для чего используется естественный вычет за пределами академии?
Я изучаю естественный вычет как часть моего Формального курса Информатики Спецификации и Проверки в Университете/Колледже.
Я нахожу это интересным, однако я изучаю намного лучше, когда я могу найти практическое применение для вещей.
Кто-либо мог объяснить мне, если и как естественный вычет используется кроме для того, чтобы официально проверить биты кода?
Спасибо!
2 ответа
Естественная дедукция не так часто используется в практических формальных методах: секвенциальное исчисление, как правило, является лучшей основой, поскольку оно ближе к табличным методам, используемым при построении процедур принятия решений для логики. Табличные методы занимают центральное место в практических приложениях логики в информатике.
Естественная дедукция чаще всего используется в конструктивной теории типов, и это дает ей некоторые возможности при разработке языков программирования. Однако это считается скорее полезным, чем обязательным.
Основная ценность естественной дедукции заключается в том, что это лучший способ изучить формальный вывод, но это дидактическое применение, которое чаще всего встречается в академических кругах.
Естественная дедукция - это очень интересно и круто, но за пределами академических кругов она очень редко используется. Формальные доказательства исправлений в программах утомительны с использованием естественной дедукции, поэтому часто используются инструменты более высокого уровня.