Re: The progress of hacking guile and prolog

[Stefan Israelsson Tampe]

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