BPF as a safer kernel programming environment

If the eBPF program is to do anything useful, it has to calculate something that isn't already calculated. In the general case, the only way to know what values it will be manipulating is to run it. C.f. the halting problem.

There's still value in assertions at the start of the program regarding its input state (e.g. a range parameter must be under a certain size, perhaps) which might be checked before execution, but that's a fairly small subset of the assertions that might be useful within the eBPF program.

The approach taken by the verifier has been to verify the subset and reject anything it doesn't know how to verify. I guess there could be a mode that understands some subset of assertions (perhaps defined declaratively in metadata alongside the eBPF program) and falls back to executing assertion statements for others but that requires some means to respond to a failed assertion during execution, which might be decidedly nontrivial in some cases...