ACL2
AbramDemski
The comments at http://news.ycombinator.com/item?id=362440 mention the
possibility of linking PLOP with ACL. I am curious. What would this
entail? What kind of interaction between them?
--Abram Demski
Moshe Looks
> The comments at http://news.ycombinator.com/item?id=362440 mention the
> possibility of linking PLOP with ACL. I am curious. What would this
> entail? What kind of interaction between them?
>
Well, this is a comparatively low priority right now and probably will
not happen for a while unless someone else takes up the baton. That
being said, there are a number of possibilities:
1) Creating a formal spec, and using it to verification the
correctness of of parts of the plop implementation - this would of
course entail rewriting such parts into applicative common lisp
(side-effect free)
2) Expanding and formalizing the theory of competent program evolution
that has been sketched by Ben Goertzel and myself (see chapter 7 of
http://metacog.org/main.pdf for some preliminaries of this theory),
and use ACL2 to specify and prove that plop implemented this theory
3) Use ACL2 within plop to attempt to prove desirable properties of
evolved programs (analogous to how human mathematicians inductively
come up with hypotheses and then use deduction to substantiate them)
As I mentioned on the hacker news thread, a friend here at Google will
probably be investigating ACL2 for plop as a 20% project (starting in
January)...
- Moshe