> 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.
I don’t think so. My hopes here are that, in having two orthogonal code bases in extremely different languages, there would be no chance that typed and untyped code intertwine, hence compromising typing accuracy. I regard this possibility as a serious problem with gradually typed languages, one of those that risk to be addressed with lengthy software engineering books, those to be mentioned as mandatory knowledge on every single programmer job interview by the year of 2039. But I digress.
“Abrupt typing” would describe this approach more precisely, if there was such jargon. A program module has no types while it is a prototype, but it must be completely typed (which is just another term for “having its correctness proved with the best tools available at this day and age”) before it goes into production.
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.