But non-exhaustively? That exists already - plenty of languages will warn or error if they can tell you're dividing by zero, but don't catch every possible case.

Any working program will in some sense be a proof, by Curry-Howard. So I think asking to not have to provide a proof is backwards; what you want is a language that makes it easy to express the program and manipulate it as a proof.