3 ms·

You don't need the tests. You need only the types. And especially you don't need "artificial dumbness", which does not understand code, and therefore won't pro

• chriswarbo 5y ago
  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!)