11–20 of 31 posts
Hmmm.. but how did the theorem prover find the solution? Probably by heuristics + brute force.
I'm disappointed. I thought I was going to see the solver generates code that finds the largest palindrome. I recall how mini-Kanren was used to generate quines. Z3 should be capable of similar feats.
Yeah, that was my first thought, too, but the article is still inspirational. Could code generation ever be fast enough for practical problems? I'm wondering how far we could get if the generated code for each problem is cached between compiles (so we build up a huge database of solutions over time) and also reused, based on the satisfied constraints, when searching for solutions to more complex problems (much like d…
Why did you need to change "(assert (and (>= a 1) (If this interests you, please do check out prolog. Declarative languages let you do something quite similar. In particular, they let you specify what you want the computer to give you rather than what you want the computer to do. Believe it or not, a very good example of such a language which you might be familiar with is SQL.
SQL is declarative only when you don't care about data integrity and performance.
Maybe a bit better example for this kind of behavior are compilers. They're pretty "declarative" these days. You write what code you want to compile, and the compiler will pass it through a thousand transformation stages, deciding which trick to apply at every instruction, which code isn't really needed and so on.
Of course, then you also need to deal with compilers getting it wrong too, so you start tweaking your code with special words like "volatile" and "restricted", mess with compiler options, and sometimes even disassemble code to see why turning the "fast" options makes your code slow. But in general, high quality compilers do this dance way better than SQL.
So what's the moral here? Two things.
First, calling something "declarative" doesn't really mean anything. It means the language is built on a very thick abstraction that lets the computer do more work than usual, so you can do less work.
Second, thick abstractions are leaky. Works for basic cases, past that you'll still end up doing a lot of work, but now you have to fight your computer while doing it, as well.
The Z3 Theorem Prover is an interesting toy, but I wouldn't trust it to do anything right in the real world. Much like most Microsoft Research projects, unfortunately.
domain(100..999).
digit(0..9).
% Variation w/ prime factors
prime(P) :- domain(P), { domain(F) : F Solving answer set programs usually involves heuristics and much work along the lines of SAT solving. Recent solvers such as clasp [1] are surprising efficient though and rival state of the art SAT solvers.
If this interests you, please do check out prolog. Declarative languages let you do something quite similar. In particular, they let you specify what you want the computer to give you rather than what you want the computer to do. Believe it or not, a very good example of such a language which you might be familiar with is SQL.
I don't believe it, because I use SQL every day, and I need to tell it which rows to lock when reading, whether to read them in share mode or fully, sometimes I need to help it figure out which indexes to use (of course I also have to manually set up the indexes too), when doing transactions I need to tell it how exactly to isolate the transaction, and I need to be very careful how I order my queries in order to avoi…
Also I wasn't suggesting that declarative languages are broadly useful (in fact I'd suggest quite the opposite), just that they are very interesting.
So, why someone don't write a stuff like this that takes your source code with tests and "builds" your app by creating the files in your dist without tests? - I write the tests - I run the compiler which transforms the tests into implementation - Run the implementation Is this even possible at all in meaningful time?
So, why someone don't write a stuff like this that takes your source code with tests and "builds" your app by creating the files in your dist without tests? - I write the tests - I run the compiler which transforms the tests into implementation - Run the implementation Is this even possible at all in meaningful time?
If this interests you, please do check out prolog. Declarative languages let you do something quite similar. In particular, they let you specify what you want the computer to give you rather than what you want the computer to do. Believe it or not, a very good example of such a language which you might be familiar with is SQL.
If this interests you, please do check out prolog. Declarative languages let you do something quite similar. In particular, they let you specify what you want the computer to give you rather than what you want the computer to do. Believe it or not, a very good example of such a language which you might be familiar with is SQL.
Granted I've only used it in one university course (and only half of that course).