Re: [Proposal] The Formal Methods in GNU Guix Working Group

[Orians, Jeremiah (DTMB)]

> I'm interested on this topic and I will try to help as much as I can.
Good
> The original idea of Brett is very interesting. In my case I would do the 
> base compiler implemented in C and using yacc (for example) to implement the 
> grammar.
> But it won't make sense in a community like Guix where most people know 
> Scheme rather than C/C++.
> So it may make sense to write a small C compiler for Scheme and then write 
> the ML bootstrap compiler in Scheme, similar to what Guix does to bootstrap 
> itself with nyacc.
Well we already have a C compiler written in scheme, it is called Gnu Mes 
(MesCC to be precise)

We also have a scheme bootstrappable from nothing written in C
https://github.com/oriansj/mes-m2
https://github.com/oriansj/mescc-tools-seed

> This will solve more problems than Guix itself, because it seems this 
> bootstrapping problem comes historically from the very first implementations 
> of ML.
Let us hope

> As we talked yesterday with Brett via chat, PolyML is the only one that has 
> been packaged in Guix but it is very tricky, because they have on the repo 
> the binaries to boostrap itself.
That needs to be fixed

> Writting a Scheme compiler should be easy, if we don't care about 
> optimization techniques. It doesn't need that requirements.
> But if you need any help in the low level area, I can help you guys.
Well I need more help in the high level areas

-Jeremiah