Given that many problems in automated reasoning are undecidable or at least not feasible in practice, there has always been a strong interest in proof assistants that can help humans to construct formal proofs. I will talk about the architecture of such systems, with particular emphasis on the LCF approach.