[blog post] Dependent types in (half of) D

[thedeemon via Digitalmars-d-announce]

On Thursday, 30 July 2015 at 16:13:46 UTC, Timon Gehr wrote:
> You need to consider the type system and the evaluation 
> semantics. What are they for the "interpreted meta-programming 
> part of D"? (I can find the semantics, but not a non-trivial 
> type system.)

Yes, this is what interests me too.

> The real difference is (roughly!) that the dependently typed 
> interpreted program always fails If there is some execution in 
> which it would fail.
> (assuming type-safety).
> "Dynamically typed" interpreted languages on the other hand 
> only fail if the particular execution exposed fails. This is 
> what we are looking at here.

I feel it too, but is this really about dynamic/dependent _types_ 
or is it about static/dynamic checking? This is probably more 
about compilation semantics than actual type system.
Also, if we have some code paths that are incorrect but never 
used during compilation, isn't it a guarantee they will never be 
used at all at runtime so the compiled program is correct? (I'm 
not sure about all this)