Как устранить ошибки из программы? Стандартная практика предлагает нам тестирование как метод нахождения ошибок в программе. Могут ли самые современные и совершенные технологии и инструменты тестирования дать гарантию того, что в программе нет ошибок? Очевидно нет. Но методология верификации - то есть математического доказательства корректности - может дать именно это. В курсе будут освещены следующие вопросы: - что такое программа как математический объект, - как определить смысл программы (также математически), - как сформулировать на формальном языке спецификацию (то есть ожидаемое поведение) программы, - как математически строго доказать, что программа удовлетворяет спецификации. По окончанию курса студенты могут выполнить практические задания с применением функционального языка flow.