eBPF and rust show that it's possible to require programs to have certain provable properties, and still have enough flexibility to write really useful programs

eBPF and rust show that it's possible to require programs to have certain provable properties, and still have enough flexibility to write really useful programs. WASM already avoids certain classes of bugs by controlling memory layout. And browsers warn if a JS script runs too long. We don't have to make software completely declarative to have safety guarantees.