If you can correctly add all the required explicit bounds checks in C what do you need Fil-C for?

It's trickier than it looks because C has mutable aliases. So, in C our bounds check might itself be a data race! Make sure you cope