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 [email protected] 在 2020年10月6日 星期二下午1:58:45 [UTC] 的信中寫道：
> 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 > <https://vlang.io> or Janet <https://janet-lang.org/> 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" <https://www.youtube.com/watch?v=OyfBQmvr2Hc> 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. > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/minikanren/6038d29e-a7d7-4e8e-9b17-1c1745d8c3fen%40googlegroups.com.
