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
