This talk will survey the state of the art in the interactive verification of basic algorithms from standard textbooks such as CLRS. Both functional correctness and computational complexity are considered and the formalization of the necessary mathematical basis for the latter is discussed.