If you're completely specifying the behaviour then you're writing a program "manually"; that's what programming is. Using a dependent type system to specify th

If you're completely specifying the behaviour then you're writing a program "manually"; that's what programming is. Using a dependent type system to specify that behaviour is essentially a form of declarative/logic programming, similar to Prolog. Deriving an implementation of those types automatically (e.g. by having the elaborator perform a proof search) is equivalent to compiling your pseudo-Prolog ahead-of-time. It's certainly interesting that such a "compiler" can be guided (e.g. via elaborator reflection), but that's more useful for optimisation rather than implementation. (Note that in some cases, such 'optimisation' might be required for the proof search to finish before the heat death of the universe!)