It's not ideal, but this post is about two different things. One is language extensibility. Another is TCB size. They are probably orthogonal.
The executive summary is that I don't find run-time type-checking interesting. And the final form of extended languages I do find interesting are Shen (similar to ML) and StrongForth (similar to Oberon). It's a research question whether using the extended lower-level language or a specifically-designed higher-level language is better. Also, I'm trying to use package repos as much as possible now, what's support like there? And should the language package repo be portable to many implementations? Significant extension packages like Shen and StrongForth aren't in repos.
All programming languages are extensible on some level, e.g. adding new functions. However, I'm interested in more deep features. The first example I saw was adding OOP support to a procedural language (Scheme). Lately I've been finding lots of examples of adding type-checkers too.
Syntactic extension, e.g. macros or templates, may be a pre-requisite for this. I'm not certain yet.
Scheme has many. So does Forth.
Yasos, a library to add OOP to Scheme
I'm primarily interested in static type-checkers (see below). Shen is an example I like. And I found a basic OOP library for it too. Coalton has a more restricted scope, I'm not sure how popular it is.
Shen programming language, can run on CL
StrongForth.f checks Forth code.
Teal checks Lua code. Mypy checks Python code (probably should have used this on a work project that had problems).
There is a group of tools that look like a static type system but actually do the checks at run-time. Although I'm sure they're useful, I'm not personally interested in these:
The standardised languages I know that can be extended to support both OOP & static typing are CL, Scheme and Forth.
The TCB of gcc, llvm or sbcl is very large. It's a bit ad-hoc, but we can assume some "degree of separation" here so that this isn't of as much concern for programs compiled in one of these compilers. Forth's lack of safety is a disadvantage; on the other hand StrongForth has one more degree of separation from a large compiler than Shen-CL/Coalton. But this metric seems a bit "woo" to me, I'm not sure it means anything. Shen-Scheme might be the best of both worlds, Chez would probably be considered "medium-size".
gcc -> gforth -> StrongForth
sbcl -> Shen
sbcl -> Coalton
Speed of StrongForth seems to be about 10x C. For reference, I assume that C++ would be about 1.5x (but with the large TCB). Shen should be similar to C++.
Maybe I should brush up on my Shen-Scheme. Even though it is updated slightly later than the CL version, it's still actively maintained.