> -- Geniepro писал(а):
> Начинать, наверное, надо с изучения литературы по таким языкам, как Coq, Agda2, тот же BitC. К сожалению, на русском такую доходчивую информацию я не видел."The Algebra of Programming" вроде как фундаментальна в этом плане, правда, говорят, трудное чтиво...
Спасибо за книжку. Хотелось бы, конечно, более доходчивого объяснения. Например, про доказательство программ на императивных языках, можно сказать, что программу надо строить параллельно с доказательством и нужно рассматривать инварианты, предусловия и постусловия.
Вот примерно так хотелось бы получить в нескольких словах общую идею верификации программ на функциональных языках.