As with Spark, proving properties over a subset of the language is sufficient. Code is written to be verified; we won’t be verifying interesting properties of large chunks of legacy code in my career span. The C (near-) subset of C++ is (modulo standard libraries) a starting point for this; just adding on templates for type system power (and not for other exotic uses) goes a long way.