I wonder if some of the Apple provided Clang annotations for bounds checking can be combined with Fil-C?

That then may allow for some of the uses to be statically optimised away, i.e. by annotating pointers upon which arithmetic is not allowed.

The Fil-C capability mechanisms for trapping double-free, and use-after free would probably have to be retained, but maybe it could optimise some uses?