Let's use miniKanren/Barliman to optimize itself?

[Steve Phillips]

Hi, all!

Intro

I'm new to miniKanren but getting up to speed quickly.  I started implementing microKanren in Go earlier today, and may implement it in V or Janet afterward.

I'm an avid Emacs user and studied Clojure years ago before deciding to keep things simple for a while by using Go for concurrent programming instead, but thanks to Will's fantastic talk "The Most Beautiful Program Ever Written" and my growing frustrations with how software is built today -- namely manually, one character at a time, often in a seriously unsafe language (like C or C++), and without our tooling being remotely intelligent nor particularly helpful -- I am looking again at Lisps and am really excited about relational programming.  Alan Kay's description of Planner and my own programming experiences has made me wonder why all programmers aren't using something like a statically (or optionally) typed Lisp with Prolog-like capabilities, and miniKanren in Scheme is closer to that than anything else I've seen (dynamic though it may be)!

Self-optimizing miniKanren?

Question: starting from a Barliman-like setup, is it computationally tractable to have miniKanren or microKanren generate a more efficient version of itself?  That is, how about giving Barliman constraints and its own source code as input, but with the slowest portion (used for program synthesis) replaced with X, thereby getting Barliman to synthesize more versions of itself, where those versions are benchmarked against each other, with the winner becoming the new running program that then (more quickly) generates faster versions of itself, ad infinitum?

Seems like a badass use case for BOINC or some SETI@Home-like network, where we all join forces to use our spare compute to make program synthesis faster and faster over time!  And hopefully without creating either Skynet or the gray goo scenario in the process :-D.

[William Byrd]

Hi Steve!

I've been thinking about doing something along these lines for a while.  Why don't we work together, and see what happens?  :)

Cheers,

--Will

--
You received this message because you are subscribed to the Google Groups "minikanren" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minikanren+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/minikanren/5bee3934-bb76-4931-a17b-f450e0a66216n%40googlegroups.com.

[zaoqi libre]

I am thinking about asking miniKanren to optimize a program and synthesize a proof in some dependently typed language to prove correctness. But it does not seem possible with available implementations

elimi...@gmail.com 在 2020年10月6日 星期二下午1:58:45 [UTC] 的信中寫道：

[silas poulson]

On Wednesday, 7 October 2020 at 04:09:26 UTC+1 William Byrd wrote:

 Why don't we work together, and see what happens?  :)

Any progress been made?

Silas