Начиная с 19 века, благодаря работам Фурье, физики использовали анализ размерностей для проверки правильности своих математических рассуждений. Основная идея состоит в том, что вы можете добавлять подобное только к подобному, поэтому вы можете добавить количество килограммов к другому количеству килограммов (или граммов), чтобы получить в сумме новое количество килограммов. Однако не имеет смысла добавлять количество метров в кубе (объем) к количеству килограммов (масса)!

Вот пример размерного анализа: если вы умножаете плотность на объем, вы получаете массу.

Анализ размерностей стал важнейшей базовой утилитой в физике, и его регулярно преподают на курсах физики студентам по всему миру, потому что он устраняет целый ряд ошибок в рассуждениях.

В разработке программного обеспечения аналогичное явление произошло с использованием систем типов. Подобно размерному анализу в физике, системы типов используются при разработке некоторых языков программирования, чтобы гарантировать, что только совместимые объекты объединяются друг с другом, обычно путем проверки совместимости параметров и аргументов функций или процедур. Не все языки включают такую ​​проверку, и поэтому программы, написанные на языках, в которых отсутствуют системы типов, с гораздо большей вероятностью столкнутся с непредвиденными проблемами, такими как «ошибки» или проблемы с безопасностью.

В PanLogica мы используем языки программирования с системами типов на протяжении всей нашей работы, но мы задались вопросом: можем ли мы развить эти идеи дальше в нашей практике разработки программного обеспечения? В конце концов, у нас есть сильное математическое наследие, и как размерный анализ в физике, так и системы типов в программировании являются средствами проверки правильности рассуждений, так что, по сути, они являются формой математического доказательства правильности.

Это приносит пользу нашим клиентам, автоматизируя проверку правильности нашего программного обеспечения помимо автоматизации тестирования, доказывая, что наше программное обеспечение не может пойти не так, где бы такие методы ни применялись.

Чтобы выйти за рамки обычных приложений систем типов, нам нужна была автоматизированная система вывода, способная конструировать доказательства новых свойств нашего программного обеспечения. К счастью, система типов используемого нами языка является полной по Тьюрингу, что означает, что это язык программирования сам по себе. Это позволило команде PanLogica внедрить новую автоматизированную проверку доказательств непосредственно в нашу практику программирования.

И результат? Мы видим, как наша работа проходит тестирование с первого раза, это похоже на волшебство! Мы поставляем самое правильное, надежное и функциональное программное обеспечение, когда-либо использовавшееся в индустрии аквакультуры, благодаря небольшой помощи силы математических доказательств.

PanLogica уже более десяти лет помогает производителям аквакультуры по всему миру, в том числе самым крупным и самым инновационным. Мы приглашаем вас связаться с нами для получения более подробной информации о Neptune и PanLogica и о том, как они могут помочь вашему бизнесу оптимизировать сроки инвестиций.

Первоначально опубликовано на blog.panlogica.com.