There is at least one language that does this as a form of its core mechanism of execution- Mercury Language, a declarative/logic programming language. Its typ

There is at least one language that does this as a form of its core mechanism of execution- Mercury Language, a declarative/logic programming language. Its type system is fairly complex. To accomplish the goal you describe, functions must be declared as deterministic, non-deterministic, or multi-deterministic. Meaning, they always have a solution, sometimes have a solution, or multiple solutions for the same input. Armed with that information, the compiler will throw an error if you haven't thought of all possibilities in your logic flow. The fact that the type system required you to be very descriptive in many different ways compounded the number of bugs that the compiler would catch before your program ever runs... I think someone said "if you can get your code past the compiler, it will work on the first try." I wish Mercury were more popular, it's an awesome project!