Hacker News Reader

For some definitions of "meaningful," yes. Per my other comment, you're describing a declarative language (prolog). Prolog is known for being ridiculously cool, and just as ridiculously slow.

That said, I think the same was true for functional languages before the folks behind GHC came along. I'd be curious to see what could happen if some substantial resources (and a few heaps of modern optimisation knowledge) were poured into this sort of language.

There is an interesting area of computer science called [inductive programming](http://en.wikipedia.org/wiki/Inductive_programming) dedicated to this sort of thing, though in a slightly different way than shown in this blog post.

Yes, you're talking about Coq. The system in this post is a fairly simple one based on unification; Coq is a full-blown theorem prover.