> use both a completely untyped dynamic language such as Tcl, where everything is a string, and a static, strongly typed programming language (ideally a proof assistant with dependent types).

This is gradual typing. The real problem with gradual typing is that you largely forgo the performance advantages of static typing, since you spend a lot of compute time translating data in and out of "dynamically-typed" (i.e. tagged/runtime dispatched) representations. This is especially obvious in stringly-typed languages ala Tcl, but applies elsewhere as well.