From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Stefan Israelsson Tampe Newsgroups: gmane.lisp.guile.devel Subject: Re: The progress of hacking guile and prolog Date: Wed, 10 Nov 2010 18:55:59 +0100 Message-ID: <201011101855.59284.stefan.itampe@gmail.com> References: <201010212223.23822.stefan.itampe@gmail.com> <87bp66q8g5.fsf@gnu.org> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: Text/Plain; charset="utf-8" Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1289412092 15682 80.91.229.12 (10 Nov 2010 18:01:32 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 10 Nov 2010 18:01:32 +0000 (UTC) To: guile-devel@gnu.org Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Wed Nov 10 19:01:28 2010 Return-path: Envelope-to: guile-devel@m.gmane.org Original-Received: from lists.gnu.org ([199.232.76.165]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1PGEz2-0004sK-Tw for guile-devel@m.gmane.org; Wed, 10 Nov 2010 19:01:28 +0100 Original-Received: from localhost ([127.0.0.1]:52698 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PGEym-00005i-3a for guile-devel@m.gmane.org; Wed, 10 Nov 2010 13:01:04 -0500 Original-Received: from [140.186.70.92] (port=34732 helo=eggs.gnu.org) by lists.gnu.org with esmtp (Exim 4.43) id 1PGEtl-0005Ts-Og for guile-devel@gnu.org; Wed, 10 Nov 2010 12:56:00 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1PGEtP-0005ri-Jx for guile-devel@gnu.org; Wed, 10 Nov 2010 12:55:46 -0500 Original-Received: from mail-ey0-f169.google.com ([209.85.215.169]:45386) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1PGEtP-0005mn-F9 for guile-devel@gnu.org; Wed, 10 Nov 2010 12:55:31 -0500 Original-Received: by eydd26 with SMTP id d26so490690eyd.0 for ; Wed, 10 Nov 2010 09:55:27 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:from:to:subject:date :user-agent:references:in-reply-to:mime-version:content-type :content-transfer-encoding:message-id; bh=cT8zFc7nLjvh+VhYT6WXdVzKzsm0fUjmdrOCYE7sdcg=; b=OvnjNJU8b/t5blk9DrVniS1NB8HWDj/2Sno5m+OcY7BzECvWADebgsr6IP36WH3acw A7svunnBCl0SsBo9C7lzEA2dbtDWiaNVdN1GlridwEXMbnx5BJ2C6plrUr6fgqQE+s9N nG59zHfaOQX54AlC4ZklKJooZZB8E9enGkw2s= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=from:to:subject:date:user-agent:references:in-reply-to:mime-version :content-type:content-transfer-encoding:message-id; b=Hw97BWmCxv4yvc3ri/t4+7adnZ1LWB4DMLQOw53IHAodBM/dq2MUSDEADxfnGYYLu+ t2lDi/ahn0XVFH0y00vV38m8Y5NmawlvT2xzon524Ga8EocAZ0Boqr1f88q5TKw96ItP kU2Tm412TYLhDruO1tzoTQeUtDE7rrUvgcK68= Original-Received: by 10.213.28.205 with SMTP id n13mr880603ebc.5.1289411726409; Wed, 10 Nov 2010 09:55:26 -0800 (PST) Original-Received: from linux-s4gz.localnet (1-1-1-39a.veo.vs.bostream.se [82.182.254.46]) by mx.google.com with ESMTPS id v51sm942168eeh.4.2010.11.10.09.55.24 (version=TLSv1/SSLv3 cipher=RC4-MD5); Wed, 10 Nov 2010 09:55:25 -0800 (PST) User-Agent: KMail/1.13.5 (Linux/2.6.34.7-0.5-desktop; KDE/4.4.4; x86_64; ; ) In-Reply-To: X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6 (newer, 2) X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.5 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Original-Sender: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.devel:11125 Archived-At: On Thursday, November 04, 2010 03:40:09 am Noah Lavine wrote: > Hello all, > > Not to derail the thread of discussion, but I've had an idea for a > feature bouncing around that I think might hook into this. I think > that Guile should offer optional static checking - not just of types, > but of everything that we can check. It could be used partly for > optimization, but partly also as a way to verify that you're reasoning > about the program correctly. (Like assert, but you prove things > correct.) For instance, > > (define (map func list) > (check (= (arity func) 1)) > ....) > > or > (define (search-binary-search-tree tree key) > (check (binary-search-tree? tree) ; or whatever conditions make sense > ....) > > I'm afraid I don't know much about how theorem provers like that would > be used to make static checkers, but is there a way to use LeanCOP or > Kanren to provide something like this? I think the easiest interface > would be one where you could put arbitrary Scheme code in check > statements, but the prover would be able to reject it as "unable to > check this", in which case it could insert a runtime check (if you > asked it to). I think that we have similar synaptical fireworks here. The actual implementation and syntax should be a result of understanding the line of reasoning in these theorem povers and checkers. So let my try to explain what I'm heading. I will try to write a little about where I am in a few days and we can continue the discussion then. > On a completely different note, I'm now looking at writing a compiler > for a subset of C, which could eventually become a JIT compiler. If we > could attach your GLIL->C compiler to that, it could produce a full > Scheme->machine code compiler in Guile. Shall we say that you implement a JIT compiler and I progress with the glil->c stuff. I was uncertain an a little afraid that I toed you here. /Stefan