Elementary Strong Functional Programming

Functional programming is a good idea, but we haven’t got it quite right yet. What we have been doing up to now is weak (or partial) func-tional programming. What we should be doing is strong (or total) func-tional programming- in which all computations terminate. We propose an elementary discipline of strong functional programming. A key feature of the discipline is that we introduce a type distinction between data, which is known to be finite, and codata, which is (potentially) infinite