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

["Orians, Jeremiah (DTMB)" <OriansJ@michigan.gov>]

> 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