OP here. It's not just Prolog, but indeed Prolog is the closest thing now.

How is it not just prolog?

At the very least, a constraint programming language would be a good basis to start with here.

http://en.wikipedia.org/wiki/Constraint_programming

I don't think there's any existing programming language that does what OP wants.

But Prolog is far from the last word on the subject. For one, it is basically untyped. There are dependently-typed programming languages that can express non-trivial properties via types, which the compiler can check (see ezyang's example).

See also:

http://stackoverflow.com/questions/2829347/a-question-about-...

Specifically, a Prolog-like syntax is also hugely popular in this fascinating Constraint Programming niche: http://en.wikipedia.org/wiki/Answer_set_programming