[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: The progress of hacking guile and prolog

From: Stefan Israelsson Tampe
Subject: Re: The progress of hacking guile and prolog
Date: Wed, 10 Nov 2010 18:55:59 +0100
User-agent: KMail/1.13.5 (Linux/; KDE/4.4.4; x86_64; ; )

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. 


reply via email to

[Prev in Thread] Current Thread [Next in Thread]