Worked example of a reduction that gets stuck due to a metafunction under the Transient semantics of Big Types in Little Runtime (POPL 2017).
Bottom line: it's tricky to pinpoint what subterm of a type is at fault when a type-tag check fails.
Type tailoring is a technique for adding domain-specific type
checkers to a typed host language. Using the Type Systems as Macros
approach to building typed languages, implementing type tailoring in
Typed Racket is straightforward. Any library can apply the core idea,
and you can try programming with type tailorings by downloading the
trivial package (requires Racket v6.4 or later).
Racket is excellent for incrementally growing scripts into full-fledged programs. This post steps through the evolution of one small program and highlights the Racket tools that enable incremental advances.
Brief summary of the seminal work by Plotkin.
Bottom line: languages and calculi must be developed together.
Also it is possible to build (inefficient) order-of-evaluation-independent interpreters; however, a call-by-value language is marginally better for the task.
Presented at PL junior.