There is this quite good EdX course developed by Gregor Kiczales, Professor of Computer Science at the University of British Columbia. It's called  How to Code: Simple Data  and it uses Racket and various modules from the book  How to Design Programs  by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt and Shriram Krishnamurthi. See this:  Review: Introduction to Systematic Program Design – Part 1  and for more on HtDP, see  Felleisen, Findler, Flatt, Krishnamurthi (Journal of Functional Programming) The Structure and Interpretation of the Computer Science Curriculum . The method consists in writing a carefully selected number of concrete test cases as examples of basic constructions and then using them to test the fully abstract representation. The approach seems, to me, to be almost  total functional programming with dependent types. See  Checking Dependent Types with Normalization by Evaluation:  A Tutorial  by David Thrane Christia...