Best I can tell, pretty much everything he describes is already part of Common Lisp. “Gradual Typing”, for example has a long history in Lisp, and is pretty much the default way to write programs.
(0) without destroying the safety guarantees of typed code,
(1) correctly assigning blame, if a runtime type error happens, to the specific untyped part of the program that causes the error.
Common Lisp's optional types don't quite fit the bill.
(check-type foo string)
When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
I know that it doesn't usually point to the line of code that is problematic, but it usually gives you a starting point for your deductions...
You don't need much from your language, except for a formal semantics. But, even if your language of choice doesn't have one, you can stick to a subset of it that is easy to formalize: no first-class procedures (or things that can simulate them, such as dynamic method dispatch), no non-local control flow operators (e.g. raising and handling exceptions), no non-lexical variables, just statically dispatched procedures and structured control flow constructs (selection and repetition, i.e., pattern matching and recursion).
> When a bug occurs (perhaps because your tests did not anticipate every edge case) how do you determine where the problem code is located without a stack trace?
By reasoning about every statement's intended and actual preconditions and postconditions, i.e., predicates on the program's free variables. At some point, the intended and actual preconditions of a statement-postcondition pair won't agree. But this is unreasonably hard if you need to reconstruct these preconditions and postconditions completely from scratch.
Your method seems impractical in the extreme in a commercial team environment.