Все же не зря мы в универе изучали конечные автоматы...это конечно только способ формальной записи по сути, но какой удобный.
@3draven конечные автоматы обеспечивают математически доказанную гарантию консистентности, но, к сожалению, даже Хаскель не позволяет эту гарантию перенести в машинный код.
Я не случайно прототип своей библиотеки FSM писал на Идрисе.
@mudasobwa если ты споришь, то неясно с чем. Если нет, ну, ок. Они не настолько хитрая штука что бы спорить.
@3draven «конечный автомат — это просто форма записи» примерно такого же уровня утверждение, как «чисел меньше нуля не бывает». В четвертом классе ждут сюрпризы.
Регулярные выражения тотальны (заканчиваются за конечное время) — только благодаря математике конечных автоматов, иначе их нельзя было бы использовать в принципе: любая регулярка могла бы вгонять код в бесконечный цикл. Таких примеров вагон.
@mudasobwa эта мысль из книги про конечные автоматы. Суть ее в том была, что императивный код, реализующий некоторый алгоритм можно написать очень по разному, но в авиации принято писать его определенным формализованным способом в виде конечного автомата. Хотя это не единственный способ записи того же алгоритма.
@3draven этот способ записи, реализованный на Idris, Agda,или Coq, в отличие от всех остальных языков, позволит формально доказать правильность реализации. Тесты будут не нужны.