Surely they knew that it would become a programming language in its own right. That's the fate of all such statically typed languages which give you type-level

Surely they knew that it would become a programming language in its own right. That's the fate of all such statically typed languages which give you type-level power but that aren't dependently typed. (Of course dependently typed languages might end up with other languages like its own tactics language.)