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

[Vicente Eduardo]

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 <address@hidden> escribió:

Hi Ludo’, all,

Thanks for your vote(s) of confidence, Ludo’; it’s great to hear!

Ludovic Courtès <address@hidden> writes:

> Hi!
>
> Brett Gilio <address@hidden> 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