Привет. Заинтересовался я функциональным программированием и математически верифицированным кодом, и конечно же, моё внимание привлек SML.
Но, во первых, мне не очевидно, какая реализация этого языка является наиболее аткуальной сейчас, позволяет создавать приложения, пригодные для использования в жизни, и при том строго соответствующей Определению.
Во вторых, мне не совсем ясно, что даёт формальная верификация. Как я понимаю, она означает соответствие программы алгоритму. Но ведь программный код и есть алгоритм, значит, если писать алгоритм сразу на ЯП, то необходимость в верификации отпадает, разве не так?
Хотелось бы на каком-то практическом примере разобрать этот вопрос.
ПС: математика - не мой профиль, так что если какие-то мат.теории нужно обязательно изучить для понимания сабжа - скажите.
