Hello,
> Though I’d recommend working on JIT for Guile before you get stuck in a
> meta-circular Curry-Howardish enlightenment period. :-)
I agree. :-)
Noah
Hi Noah,
On Wed 24 Nov 2010 02:54, Noah Lavine writes:
> What I'm thinking of is like racket contracts, but with the idea of
> "trusted modules", which might involve static checking.
Yeah, definitely. Like the interface between typed and untyped code in
racket, also. I don't know very much abou
Hi!
Noah Lavine writes:
> What I'm thinking of is like racket contracts, but with the idea of
> "trusted modules", which might involve static checking. For instance,
> if the contract is that map's second parameter is a list, you'd
> normally want to check that. But if a module that used map cou
Hi Noah,
On Wednesday, November 24, 2010 02:54:37 am Noah Lavine wrote:
> Hello,
>
> That might make sense. The documentation certainly looks interesting.
>
> What I'm thinking of is like racket contracts, but with the idea of
> "trusted modules", which might involve static checking. For instanc
Hello,
That might make sense. The documentation certainly looks interesting.
What I'm thinking of is like racket contracts, but with the idea of
"trusted modules", which might involve static checking. For instance,
if the contract is that map's second parameter is a list, you'd
normally want to c
Hi again,
The more apropos link to Racket's contracts would probably be:
http://docs.racket-lang.org/guide/contracts.html
Cheers,
Andy
--
http://wingolog.org/
Hi Noah,
On Thu 04 Nov 2010 03:40, Noah Lavine writes:
> I think that Guile should offer optional static checking - not just of
> types, but of everything that we can check.
It seems like you're really asking for *dynamic* checking -- not only
checking properties that can be proved statically,
> Interesting. I thought you were going rather to compile a subset of
> Scheme to C, which could be used to implement VM instructions, no?
Yes, that was my plan, sorry. I want to compile things to C, not from
C to machine code.
Also, to clarify, I am looking at compiling not a subset of C, but
s
Yes, that's right. I was unclear. I am intending to come up with a
language that I can compile to C, to implement VM instructions. I
meant I would compile something to C, not from it to machine code.
Just to clarify, it probably won't be a subset of Scheme (although one
could compile a subset of S
Hello,
> 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
Hi,
Noah Lavine writes:
> 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.
Interesting.
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 ev
Ok, for the c generator, here are some code attached. I would
just study this there is bit's still missing and you need to wait for me to
dig up the details. My point is to suggest ideas for what can be done.
I don't assume that this is it. But it's a nice playing ground.
So it is a hack, here
On Thursday, November 04, 2010 12:43:54 am Ludovic Courtès wrote:
> Hi Stefan,
>
> Lots of stuff here, which is why I took the time to read it. :-)
>
> Stefan Israelsson Tampe writes:
> > 1. The theorem prover (leanCop) is a nice exercise
>
> [...]
>
> > 2. Kanren is a nice way to program lik
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
Hi Stefan,
Lots of stuff here, which is why I took the time to read it. :-)
Stefan Israelsson Tampe writes:
> 1. The theorem prover (leanCop) is a nice exercise
[...]
> 2. Kanren is a nice way to program like with prolog,
Great that you’re mentioning them. It looks like there’s a lot of
i
Hi,
I think it's good to discuss what I do with the prolog and unifer. So this
is what I've been doing.
1. Incorporate a theorem prover for extension and playing
2. Kanren like hygienic macro package
3. Make the c-code variables printable and hence much less segfaults at bt :-)
e.g. robustify
17 matches
Mail list logo
