I’ve thought about how to let folks prove to Fil-C that Fil-C’s checks are obviated by some higher level checks.

It’s a super hard problem! I don’t have a good answer, but I also can’t prove that it’s impossible

If you have an interpreted language, you don't have a C function corresponding to each language function. You have a C interpreter loop with a "current instruction" pointer. When the current interpreted instruction is a call, you check all the things you need to check, push the current IP to a stack, and set the IP to the first instruction of the function.

C's type checker never sees the interpreted language's functions.