Хоар, Чарльз Энтони Ричард - великий ученый, внесший большой вклад в информатику.

Мне понравилась его статья An Axiomatic Basis for Computer Programming. Написана доступным языком и в общих чертах определяет пути доказательства программ. Удивительно как человеку удалось формализовать в аксиомах, утверждениях и теоремах, то как я убеждаюсь в корректности своих программ. Я понял, что делаю это недостаточно формально, не отдавая себе отчета в истинных посылках и следствиях. И в статье показано, как это можно исправить.

Статья очень много цитируется и по ней можно найти огромное количество материалов, связанных с формальным описанием языков и программ на них.

Хоар является автором множества других интересных статей.