The driving idea of functional programming is to make programming more closely related to mathematics. A program in a modern functional language, such as Haskell or Miranda, consists of equations, which are simultaneously computation rules and axioms for reasoning about the entities thus computed.
In this talk I will argue that our existing model of functional programming, although elegant and powerful, is mathematically compromised - to a much greater extent than is commonly recognised - by the presence of partial functions. I will sketch a proposed discipline of total functional programming, based on introducing a sharp distinction, enforced by the type system, between data and codata.