Universal vs. existential properties of programs

There's an age-old debate about whether abstraction is an absolute necessity or an obstruction to programmer efficiency. It shows up in the static-vs.-dynamic typing war, the abstract datatypes-vs.-concrete representations war, etc. I've always suspected we'd be worse off if we let one side or the other win. Of course I don't claim to know how to resolve it, but I wonder if it would shed light on the issue to think about existential vs. universal properties of programs.

When you're debugging or testing code ("is it possible for this list to be empty?"), or when you're exploring an API at the REPL ("what happens when I pass the result of Foo to Bar?"), you're often looking to observe a single program trace that serves as a witness to an existential property. By contrast, when you're building robust systems, you often want to assert universal propositions about the code ("this function will only ever produce a non-negative integer").

When you're building a system, you want your invariants to be universally true. This is one place where enforcement of abstractions (as with static type systems) is important. Letting the software enforce the abstractions automates the process of verifying these properties.

When you're inspecting a system, though, you're often looking for particular, concrete examples. In my experience, people are better at going from the particular to the general rather than vice versa. I don't think we tend to think well in abstractions; at least not at first. That's why verifiers that work by searching for counterexamples produce such good errors: instead of directly proving ∀x.P(x), they try to prove ¬∃x.¬P(x), and if they fail, they give you a concrete x. Learning API's, interacting with the REPL, and writing test cases are all examples of this mode of programming where you're more interested in concrete paths through a program rather than universal properties.

How would we design software that facilitates both these modes of reasoning about programs?