Does that mean social housing would only be accessible to Celtic people, excluding recent immigrants such as Angles, Saxons, Vikings, …?

We’re talking about different kind of proofs.

Proving a program is correct requires a formal specification and a formal verification with mathematics and/or formal methods. ie proving the behavior and result perfectly match specification for all possible inputs.

A test only proves that a program 1) returns the expected output for a specific input, or limited set of inputs, and 2) appears to behave correctly, ie there may be undefined behaviour but they don’t cause an immediate crash.

Actually proving that C code is correct is not easy.

Having a human developer manually write code that is less harmful/wrong, and doesn’t require proof, is probably easier.