5 ms·
An interesting vision is that we'll go from programs that can be executed to models that can be solved with generic solvers (e.g. SAT solvers [1], or CP solvers
by bnegreve 11y ago
An interesting vision is that we'll go from programs that can be executed to models that can be solved with generic solvers (e.g. SAT solvers [1], or CP solvers [2])
So if you need to sort an array, instead of programming quicksort, you will simply specify that you are looking for a permutation of the input array T such that for all i, T[i] < T[i+1] and the solver will search and find a solution to your problem (i.e. a sorted array) using whatever technique it likes.
Many constraint satisfaction and optimisation problems are already solved this way, there's a possibility that this generalise to other problems.
There's many advantages to this: first you need less (no?) testing, because if the solution doesn't match the problem specification it can only be a bug in the solver.
Second, there's a chance that solvers will eventually be as fast as human programmers at finding solutions. Just like the compilers are almost as good at programmers at generating assembly, and often better. If this happens programming in general will become as useless as programming in assembly today.
[1] http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Algorithms_for_solving_SAT http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#...
[2] http://en.wikipedia.org/wiki/Constraint_programming http://en.wikipedia.org/wiki/Constraint_programming
- skierscott 11y agocvxpy[1] is a good example of this. The contraints are specific symbolically and cvxpy optimizes for you (assumes problem is a convex optimization problem etc) [1]:https://github.com/cvxgrp/cvxpy https://github.com/cvxgrp/cvxpy
- bnegreve 11y agoYes, there are many of these. I think MiniZinc is also quite popular among the optimisation guys http://www.minizinc.org/ http://www.minizinc.org/
- platz 11y agoReminds me of Expert Systems
- vezzy-fnord 11y agoWhy hasn't Prolog programmed us out of existence, then? Don't get me wrong. Constraint solvers are useful and powerful tools for declarative problem solving, but I don't recall them ever being viewed as general-purpose, especially not to the level of being a generic "autocode" (what compilers were once called, funnily enough) system. Genetic programming seems like a more likely candidate (with some combination of SAT solvers and statistical learning), but again hypothesizing about such a major thing doesn't appear fruitful at present.
- bnegreve 11y agoTo clarify CP and SAT solvers are just examples and obviously they're not good enough otherwise we would be using them already. Genetic programming with combinations of SAT and statistical learning is also a possibility I guess [1]. The point is that you wouldn't need to instruct the processor what to do anymore, you would just specify the output (aka declarative programming). > Why hasn't Prolog programmed us out of existence, then? I would say because of its (low) speed. > Constraint solvers are useful and powerful tools for declarative problem solving, but I don't recall them ever being viewed as general-purpose, especially not to the level of being a generic "autocode" They are not autocode, but they are autosolve-my-problem which is in fact what you really want. I don't believe automatically generating code makes any sense. Source code is a very inefficient way to represent a program (i.e. a function) that is only useful because it can easily be written/modified by humans. There's no point in using source code as an internal representation for a program. [1] AFAIK state of the art SAT solvers already do some level of learning: http://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning http://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning