The main point is separation of responsibilities. The kernel verifier should simply ensure the kernel's availability, but it shouldn't get into the business statically analyzing memory safety for data structures the program maintains for its internal state. That is both hard to do (in a language independent way at the bytecode level), and also undesirable. We would have to enforce some sort of aliasing regime that is unnatural (except perhaps in Rust) to enable local reasoning.

In the future, we may want even stronger functional correctness for, say, BPF CPU schedulers. It would be easier to compose and lift existing toolchains (Dafny, Verus) in user space and compile them down to native languages (which then successively compile down to BPF bytecode), rather reinventing all that and shoving a SAT solver to discharge more complex verification queries from the kernel verifier. It may be so that not everyone needs such strong guarantees (esp. during development). Optionality and clear distinction of responsibilities seems like a more sustainable long term approach for the ecosystem.

> If normal C is easy to write, it's unsafe.

I think the way to address this is to use a better language than C to write kernel extensions, and layer memory safety for extension's own state on top of the guarantees BPF already ensures for the kernel resources and interfaces. Eventually the Rust frontend for BPF should become a thing (it's WIP), which would hopefully be an improvement. You could argue Rust is not perfect and still leaves much to be desired, but it has primitives that allow you to negate presence of memory safety issues (as long as unsafe code is not violating that property) in a decidable fashion for BPF program's arena accesses. The kernel verifier already presents a restricted interface into the kernel and makes sure things are correct when accessing kernel objects.

> Instead of making BPF look more like userspace, I'd make it easier to integrate BPF *with* userspace,

This is how it works already. Several use cases you pointed out (schedulers in particular) already have much of their logic in user space.