No post body was provided.
Untitled topic
1–10 of 31 posts
Re: undefined
#2Hmmm.. but how did the theorem prover find the solution? Probably by heuristics + brute force.
Re: undefined
#3Hmmm.. but how did the theorem prover find the solution? Probably by heuristics + brute force.
"Z3 integrates a modern DPLL-based SAT solver, a core theory solver that handles equalities and uninterpreted functions, satellite solvers (for arithmetic, arrays, etc.), and an E-matching abstract machine (for quantifiers)"
From http://research.microsoft.com/en-us/um/redmond/projects/z3/z...
Re: undefined
#4Hmmm.. but how did the theorem prover find the solution? Probably by heuristics + brute force.
I'm not sure which one exactly, but it's a SAT solver, so it uses a SAT solving algorithm [1].
1 - http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#...
Re: undefined
#5I'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.
Re: undefined
#6I'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 developers reuse existing functions).
Re: undefined
#7So, 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?
Re: undefined
#8If 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.
Re: undefined
#9recently i was tinkering with the idea vedil.wordpress.com/2014/07/09/test-driven-program-synthesis/
is this feasible?
Re: undefined
#10So, 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?
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.