Most programming is still ad-hoc. Even if somebody has an "architecture" for a project, chances are there's still a zillion things that aren't remotely statically checked.

What can/not be? depends on many things of course, but I wish there were a table, chart, venn diagram, whitepaper, or something that listed the ideas of what bugs can be statically checked. What if Maslov wrote about the hierarchy of needs of good computer systems? What if we start with non-turing completeness and see what we can assure, and then see what options we have if we start to 'fall back' into the turing mud pit.

Things I'd hope for; things that tend to be buggy:

+ order of operations.

+ type mismatches.

+ null.

+ over/under flow.

+ collection bounds checking.

+ concurrency: races, deadlock, livelock, determinacy.

+ performance.

+ security.

+ extensibility, eg algebraic compositional properties.

+ support for aspect oriented, cross-cutting concerns.

+ end-to-end data models.

+ versioning of any/everything.

+ cross-platform-ness.

+ reusability, or at least fuzzy logic copy-paste code detection.