> It's not beyond hope that we could find a subset that allowed us to write most useful programs but was easier to reason about.

It is beyond hope that we find a subset that's generally easier to reason about. Verifying one line programs of this sort:

if (a && ~b || c || ~d && e ...)
crash()

is already NP-complete (SAT). Adding some loops that are of depth 2 makes it PSPACE-complete (TQBF, aka QSAT). I can't think of a useful programming language that doesn't have even small-constant-depth loops (which makes it finite state) and simple boolean algebra. Software verification is about verifying some subsets of programs that humans happen to write. It is categorically impossible to write a general-purpose language where all programs are easier to verify than PSPACE.

> but can't we just make that one of the properties we keep track of and prove with the same tools?

Sure, with super-exponential complexity :) But again, this is in the worst case. We hope that humans usually write programs that are simpler.

> I guess my experience that keeping track of more properties in the type system doesn't make coding any harder.

If you mean H-M types as in Haskell, then the properties those types enforce are either trivial (i.e. true for all programs, e.g. function returns Int), or a result of a finite state machine (that's the proving strength of H-M types). You cannot prove even a single bit of a program's output that's a result of non-constant-depth recursion (there's a special case for recursion which is of depth that's a constant multiple of the input length, like `map`). If we take Haskell, you can replace each of your functions with constant-depth recursion (0 or 1 would suffice in virtually all circumstances) and the program will still typecheck yet will be completely wrong.

As for Rust's linear types, that is precisely what I'm talking about. A certain class of bugs (memory errors) that humans are known to make and that verifying with abstract interpretation is easy. That's what software verification aims to do. We cannot hope of proving general programs generally correct, regardless of the language they're written in.

BTW, thinking of type systems muddles understanding in this case, because type systems are just notation. The verification taking place in most sound type systems is abstract interpretation. Yes, we can find more important properties to verify with abstract interpretation, but it has been proven that some properties will forever elude abstraction.

The way abstract interpretation works is that it translates the program into an "abstract" program which is just a finite state machine, with the number of states equal to the number of concrete types, and running an exhaustive model checker on that; this means that the complexity of inferring this kind of types is Ω(|S|), namely, linear in the number of concrete types. As abstract types can multiply the number of concrete types, the inference can become exponential in the worst-case, but it usually doesn't. Once you introduce dependent types, the algorithm is still Ω(|S|) -- linear in the number of state, i.e. types -- but now the number of types is unbounded, and so the problem becomes undecidable.

> until writing a program naturally includes proving the important properties of that program without even noticing.

You're right, but this entirely depends on which properties are found to be important (and has little to do with type systems specifically; again, this is mostly notation[1]), and that, in turn, is rather empirical.

[1]: Not entirely, though, but mostly.