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

[Brett Gilio <brettg@posteo.net>]

Jack Hill <jackhill@jackhill.us> writes:

> I'm not a formal methods researcher, but merely a hobbyist who is
> interested in programming languages and type system. That said, I find
> this proposal intriguing, and would like to follow along, and perhaps
> help as I am able. At the very least, I hope to learn some new things.

I am glad you say this. We all have a lot to learn from each other here.

> One of the things that attracted me to Guix is the ability to
> represent the pieces as objects in a programming language as opposed
> the the big mass of state that is a traditional system. I agree this
> property of Guix harmonizes with formal analysis.

Absolutely! This is the kind of thesis I was proposing, and something
that I wonder what Julien will think of as far as benefits particular
and specific to the formal methods community.

>> What follows is proposals for some of the work to be done by this
>> working group:
>>
>> -- A lot of proof assistants are based on dialects of ML. Most of these
>>   use SMLnj or MLton for their work. To date there is an issue of
>>   source-based bootstrapping of _all_ of the major ML compilers. We do
>>   have PolyML in our repositories, but even this uses space-inefficient
>>   text file blobs for compiling and is not a fully C-based source
>>   bootstrap. Basically, all of the ML compilers rely on some distinct
>>   pre-compiled something-or-other to get to their pristine state. I
>>   have explored the idea, along with Leo and Amin, about following in
>>   the tradition of MES (and mrustc) and starting an analogous GNU project for
>>   writing a reduced-size specification ML bootstrapping compiler. That
>>   way we can end the loop of a source-based build of ML97 compilers
>>   being basically impossible.
>>   [See issues #38605 & #38606 on DEBBUGS. Also, see
>>   https://github.com/MLton/mlton/issues/350.]
>
> This is the sub-area I'm most interested in. In addition to ML, I'd
> also like to be able to bootstrap GHC. I know that Ricardo has done
> some work in that area [0].
>
> [0]
> https://elephly.net/posts/2017-01-09-bootstrapping-haskell-part-1.html

So far this idea has garnered the most attention. Amin Bandali and I are
both wanting to see this be taken to the next level, with maybe the
support of Janneke and other people working with minimal compilers /
formal methods in their day-to-day work. See some of my previous emails
to others about why I think this is important work. Basically, as I
mentioned to Ludo' the situation of bootstrapping ML from source is
occluded after 1993. We should reasonably be able to remedy this in
order to facilitate ML-based proof assistant development and use on
Guix. Especially things like the PRLs (NuPRL, RedPRL, JonPRL) which
offer nice dependent type systems. But first the compiler tower needs to
be there."

Maybe we could borrow some inspiration from miniML (mentioned by
Julien), CakeML (mentioned by Simon), or C Minor? I don't know. But I
think this is an important task.

> Thanks for proposing the idea!
>
> All the best,
> Jack

Thank you for voicing your support Jack! :)

-- 
Brett M. Gilio <brettg@posteo.net>
GNU Guix, Contributor <https://guix.gnu.org/>