I think the Julia people were right to remove "dependent" from the docs. Nowadays I say that Julia has a limited form of static dependent typing, which is to say it doesn't have dependent typing.

When we first wrote Nemo in Julia, we used a form of emulated dependent typing. But the way we did this led to performance problems that we just hadn't thought about.

For example, if we did lots of operations over Z/pZ for many primes p, e.g. in multimodular algorithms, it meant that the Jit compiler had to recompile everything for every prime p, which was awfully slow.

Julia is absolutely not meant to be used that way, and it took us a long time to see that. After redesigning Nemo to use Julia much more like the way it was designed to be used, we actually ended up speeding everything up.

My own research was partly working to integrate LISP's and imperative programming. Seeing it already happen some way in Julia is totally awesome! I'll have more praise for it in the future I see. Ok, for dependent types, it doesn't have dependent types but one or more pieces of that capability? Maybe more once I've read the linked pages.

Thanks for the answer and links!

Edit: Just read the debate. I agree with 'tel' that the phrase dependent types has such a specific meaning, capabilities, and whole literature devoted to it that nobody should use it unless it's consistent. The Google search point was especially smart. Per that discussion, not my own analysis of Julia, Julia doesn't have dependent types & it's good they took that phrase off the site. Its different enough to justify a custom term to promote its usefulness while not misleading.