Понятие знание, которое используется в компьютерной науке, не включает в себя обычное для философской эпистемологии требование обоснования знания. Такое положение вещей имеет глубокие корни в истории философской логики в XX в. и приводит к негативным практическим последствиям. Исследования последних лет в области теоретико-доказательной семантики, гомотопической теории типов и формальной эпистемологии позволяют наметить теоретическую основу для решения этой проблемы.