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

[Vicente Eduardo <vic798@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2969 bytes --]

I'm interested on this topic and I will try to help as much as I can.

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.

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

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.

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.

Vicente.

El sáb., 28 dic. 2019 8:21, Amin Bandali <bandali@gnu.org> escribió:

> Hi Ludo’, all,
>
> Thanks for your vote(s) of confidence, Ludo’; it’s great to hear!
>
> Ludovic Courtès <ludo@gnu.org> writes:
>
> > Hi!
> >
> > Brett Gilio <brettg@gnu.org> skribis:
> >
> >> 100% Agreed. Amin is also working on packaging the Lean prover and I am
> >> taking an interest in seeing if we can extend the OPAM importer to have
> >> a subimporter for Coq.
> >
> > That’d be nice!
> >
>
> I just sent in the very first patch inspired (in part) by this proposal
> to guix-patches: https://issues.guix.gnu.org/issue/38770 :-)
>
> >
> >> Ludo, what do you think about an https://fm.guix.gnu.org/ URL hosting a
> >> haunt webpage designed by Amin and I (and maybe others) to detail the
> >> purpose, goal, and maybe institutional use cases (research papers) of
> >> GNU Guix in the formal methods community?
> >
> > The domain name would have to be discussed with others (other
> > maintainers in particular; perhaps a better choice would be
> > formal-methods.guix.info or fm.guix.info, next to hpc.guix.info), but
> > the idea sounds great to me!
> >
>
> Sure!  I’d love to hear from others (esp. other maintainers) about this.
>
> Personally, being a GNU maintainer, webmaster, and Savannah hacker, I’m
> (almost by definition :-)) partial to using *.gnu.org and various pieces
> of the GNU infra (lists, Savannah source repositories, …) for GNU work
> whenever possible.  As such, I naturally like fm.guix.gnu.org better as
> the domain, and would prefer to use Savannah for hosting our sources,
> e.g. the Haunt sources for the Guix-FM site.
>
> What do you think?
>
> Like Brett, I’d be curious to hear the reasons for using *.guix.info and
> a non-Savannah repository forge for Guix-HPC.
>
> >
> > Thanks,
> > Ludo’.
>
> Best,
> amin
>

[-- Attachment #2: Type: text/html, Size: 4459 bytes --]