[Proposal] The Formal Methods in GNU Guix Working Group

[Proposal] The Formal Methods in GNU Guix Working Group

[Alexandru-Sergiu Marton]

Hi all,

I know I'm a bit late to the party but I want to express my support
for this initiative.

I have very little knowledge about formal methods - extracted from
this thread, a few conversations with Brett and from skimming through
the Wikipedia page. Despite this, I find the idea of a Formal Methods
Working Group in GNU Guix being very interesting and I think this
environment suits such a trade very well.

You have my support (like from a cheerleader, because I don't have the
technical knowledge to provide other kinds of support). I'm looking
forward to hearing more about this working group and it's activity.

Cheers,
Sergiu

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

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

[zimoun]

Dear,

On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
<OriansJ@michigan.gov> wrote:

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

The term "nothing" is mitigated; i.e. "nothing" means: a booted system
running a (linux) kernel. Right?


Thank you for all your contributions!
e.g., hex0 is amazing! :-)

All the best,
simon

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

[Svante Signell]

On Wed, 2020-02-12 at 15:16 +0100, zimoun wrote:
> Dear,
> 
> On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
> <OriansJ@michigan.gov> wrote:
> 
> > We also have a scheme bootstrappable from nothing written in C
> > https://github.com/oriansj/mes-m2
> > https://github.com/oriansj/mescc-tools-seed
> 
> The term "nothing" is mitigated; i.e. "nothing" means: a booted system
> running a (linux) kernel. Right?

I do also suspect that mes* is only for Linux so far. Any plans for Hurd? Or are
the old bootstrap binaries still needed (when non-corrupt)?

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

[Jan Nieuwenhuizen]

Svante Signell writes:

> On Wed, 2020-02-12 at 15:16 +0100, zimoun wrote:
>> Dear,
>> 
>> On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
>> <OriansJ@michigan.gov> wrote:
>> 
>> > We also have a scheme bootstrappable from nothing written in C
>> > https://github.com/oriansj/mes-m2
>> > https://github.com/oriansj/mescc-tools-seed
>> 
>> The term "nothing" is mitigated; i.e. "nothing" means: a booted system
>> running a (linux) kernel. Right?
>
> I do also suspect that mes* is only for Linux so far. Any plans for Hurd?

Your suspicion is somewhat correct.  GNU Mes v0.22 added initial support
for the Hurd, and introduced a FreeBSD scaffold.  Support for the Hurd
has always been the plan, see the Guix ROADMAP or the manual
(https://guix.gnu.org/manual/en/html_node/operating_002dsystem-Reference.html#FOOT23).

Greetings,
janneke

-- 
Jan Nieuwenhuizen <janneke@gnu.org> | GNU LilyPond http://lilypond.org
Freelance IT http://JoyofSource.com | Avatar® http://AvatarAcademy.com

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

[Bengt Richter]

Hi Guix,

On +2020-02-12 15:16:47 +0100, zimoun wrote:
> Dear,
> 
> On Wed, 12 Feb 2020 at 13:03, Orians, Jeremiah (DTMB)
> <OriansJ@michigan.gov> wrote:
> 
> > We also have a scheme bootstrappable from nothing written in C
> > https://github.com/oriansj/mes-m2
> > https://github.com/oriansj/mescc-tools-seed
> 
> The term "nothing" is mitigated; i.e. "nothing" means: a booted system
> running a (linux) kernel. Right?
>

ISTR someone made an initrd with guile in it, and "booted to guile."
If that is so, does that not suggest that "from nothing" could
be independent of a running kernel?

Wouldn't that be cool? !! ;-)

> 
> Thank you for all your contributions!
> e.g., hex0 is amazing! :-)
> 
> All the best,
> simon
> 

-- 
Regards,
Bengt Richter

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

[Orians, Jeremiah (DTMB)]

> ISTR someone made an initrd with guile in it, and "booted to guile."
Yep amazing work that it is; someone also made emacs an initrd too

> If that is so, does that not suggest that "from nothing" could be independent of a running kernel?
Actually no, bare metal is a bit different than running on top of a posix
But is even more fun is we made a 737byte initrd/shell
https://github.com/oriansj/bootstrap-seeds/blob/master/kaem-optional-seed.hex0
Which means one can bootstrap on POSIX from hex0 and the above all the way to mes-m2

> Wouldn't that be cool? !! ;-)
Indeed, hence why the solving of the Linux/POSIX bootstrap problem can be solved with M2-Planet and stage0
Need more help though to get it all done faster

-Jeremiah

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

[Orians, Jeremiah (DTMB)]

> The term "nothing" is mitigated; i.e. "nothing" means: a booted system running a (linux) kernel. Right?
No, I mean bootstrapped from bare metal.
No Kernel
No firmware
No microcode
No Bios
Just individual TTL logic circuits
https://github.com/oriansj/stage0

> Thank you for all your contributions!
> e.g., hex0 is amazing! :-)
Hex0 is only about 3 hours of work
This however is taking me months
https://github.com/oriansj/mes-m2
and when done will result in solving multiple bootstrapping problems

-Jeremiah

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

[zimoun]

Dear,

On Thu, 13 Feb 2020 at 13:07, Orians, Jeremiah (DTMB)
<OriansJ@michigan.gov> wrote:
>
> > The term "nothing" is mitigated; i.e. "nothing" means: a booted system running a (linux) kernel. Right?
> No, I mean bootstrapped from bare metal.
> No Kernel
> No firmware
> No microcode
> No Bios
> Just individual TTL logic circuits
> https://github.com/oriansj/stage0

Is it ready yet?
This should be great. :-)


All the best,
simon

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

[Orians, Jeremiah (DTMB)]

>> > The term "nothing" is mitigated; i.e. "nothing" means: a booted system running a (linux) kernel. Right?
>> No, I mean bootstrapped from bare metal.
>> No Kernel
>> No firmware
>> No microcode
>> No Bios
>> Just individual TTL logic circuits
> Is it ready yet?
Well the parts all the way to M2-Planet are done and verified on the virtual machine
https://github.com/oriansj/stage0

We however need to write a portable POSIX to remove Linux from guix's bootstrap
(Ideally buildable via M2-Planet and discussion on what route is ongoing)

Then implement the design on FPGA via http://www.clifford.at/icestorm/

Finally I'll have to convince my wife to let me spend $10K to implement the design in hardware using: https://libresilicon.com/
(But at least I'll have plenty of free chips to share with the world)

>This should be great. :-)
That is the plan but we really could use more scheme programmers.
(Ambitious goals and all that)

-Jeremiah

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

[zimoun]

Dear,

Thank you for the explanations.

On Tue, 18 Feb 2020 at 12:17, Orians, Jeremiah (DTMB)
<OriansJ@michigan.gov> wrote:

> Finally I'll have to convince my wife to let me spend $10K to implement the design in hardware using: https://libresilicon.com/
> (But at least I'll have plenty of free chips to share with the world)

Maybe I could try some sort of crowd funding...


All the best,
simon

[Proposal] The Formal Methods in GNU Guix Working Group

[Brett Gilio]

Hello Guix!

This is going to be a rather lengthy email proposing a new working group
(if that is indeed the proper name for this) in the GNU Guix
project. Just as there are other "working groups" for GNOME packages,
bootstrapping Rust & JVM, and bootstrapping the entirely of the GNU
Corelibs (GNU Mes) in Guix, I am proposing a new working group based on
the synthesis of two fundamentally and mutually agreeable concepts.

This is a continuation of the discussion proposed by Amin Bandali, Leo
Prikler, and I from the #guix Freenode IRC. All three of us are either
students of formal methods in mathematics and computer science, users of
proof assistants, or interested in category theory and type theory. As
such as noticed and wondered what kind of community there is for formal
methods in GNU Guix, and by extension what kind of benefits GNU Guix has
to offer the formal methods community which is providing some of the
most rigorous research in computing methods to date.

First, some background. For those of you unfamiliar with formal methods
and software verification in computer science, it is by-and-large
applications of mathematical proof to the conceptions of how we design
our software. We design our software around proofs that have a certain
level of correctness thus we do not have to speculate about the behavior
of that software. To me that has a striking resemblence to the less
rigorous but all-the-more impressive goal of Guix to be functionally
deterministic. Many of the concepts of formal methods take from untyped
(and typed) lambda calculus and are then abstracted to have higher-order
guarantees in their construction.

Having Guix and the Formal Methods community aligned would mean a great
deal of power for both camps! Just as we see with the Software Heritage
project and Guix, for providing historical and state-consistent
reproducible environments for software testing we and correspond to
formal methods much of the same guarantees of deterministic
computational states, modeling, and reasoning in software correctness.

Amin, Leo, and I all likely agree that _some_ relationship here is good
to be opened and explored! I know that there are some of us who come
from institutions that have historical relationships to the proof
assistant community, Caml, HOL (looking at you Ludo', though IIRC you
are in a different working group at INRIA),
so this could be more of a chance to see bigger institutions begin to
adopt Guix for their research work.

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.]

-- Begin adding more projects that are important works in the formal
   methods community. We have Coq, Idris, and Agda, but there is a lot of work
   to be done on keeping these projects not only up-to-date but also
   adding subprojects that use these toolchains. For example: C Minor,
   Metamath, Ynot, Formally verified Featherweight Scala, RustBelt,
   RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of
   various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid
   Haskell, extensions to Z3, and tons more!

-- Possibly begin formally verifying some of the behavior and
   implementations of GNU Guix and GNU Guile. This is kind of an add-on
   idea, but it struck our interest so why leave it out?

-- Begin giving talks on the benefits of GNU Guix at conferences around
   Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

All of this seems really nice and impressive, but what is it without
getting some feedback from the community? I'd _really_ love to hear your
thoughts, experiences, and more on this working group idea and other
working groups to avoid pitfalls. Maybe we should have a secondary
#guix-fm channel on IRC? There is definitely a lot of work to be done
here, and we will need some form of organizational structure to keep the
work consistent and neatly integrated with the goals and purposes of GNU
Guix.

I hope to hear from the community.

Thanks,

-- 
Brett M. Gilio
Homepage -- https://scm.pw/
GNU Guix -- https://guix.gnu.org/

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

[Julien Lepiller]

Le 16 décembre 2019 01:59:59 GMT+01:00, Brett Gilio <brettg@posteo.net> a écrit :
>Hello Guix!
>
> ...
>
>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.]
>
>-- Begin adding more projects that are important works in the formal
>methods community. We have Coq, Idris, and Agda, but there is a lot of
>work
>   to be done on keeping these projects not only up-to-date but also
>   adding subprojects that use these toolchains. For example: C Minor,
>   Metamath, Ynot, Formally verified Featherweight Scala, RustBelt,
>   RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of
>   various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid
>   Haskell, extensions to Z3, and tons more!

OCaml stuff can easily be imported with guix import opam. I know coq packages use a separate opam repository, so it would be nice if the importer could take an optional parameter to indicate a custom opam repository url. I'm not sure the coq repo is converted to opam 2 yet though.

>-- Possibly begin formally verifying some of the behavior and
>   implementations of GNU Guix and GNU Guile. This is kind of an add-on
>   idea, but it struck our interest so why leave it out?
>
>-- Begin giving talks on the benefits of GNU Guix at conferences around
>   Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

I can see the benefits of formal methods and benefits of guix, but what does guix provide or could provide to formal method people specifically? Is it "only" the nice guarantees it gives to any programer, or is there something else? Maybe the question is why does it matter more to fm people than to other programmers?

>All of this seems really nice and impressive, but what is it without
>getting some feedback from the community? I'd _really_ love to hear
>your
>thoughts, experiences, and more on this working group idea and other
>working groups to avoid pitfalls. Maybe we should have a secondary
>#guix-fm channel on IRC? There is definitely a lot of work to be done
>here, and we will need some form of organizational structure to keep
>the
>work consistent and neatly integrated with the goals and purposes of
>GNU
>Guix.

I think we're still a small community, so we can continue talking about it on the main channel. We're trying to avoid dividing information, that's why we allow any language on tge channel, instead of having separate chans for each language. We also always hear about bootstrapping or the hpc effort on the main channel. Let's talk about fm :). You can count me in.

>I hope to hear from the community.
>
>Thanks,

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

[Julien Lepiller]

I forgot to metion I have a small channel at https://framagit.org/tyreunom/guix-coq-channel that keeps track of every coq version since 8.6. I use it to test my coquille plugin on every coq version that exists, but I'm sure there are other use cases :)

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

[Brett Gilio]

Julien Lepiller <julien@lepiller.eu> writes:

> I forgot to metion I have a small channel at
> https://framagit.org/tyreunom/guix-coq-channel that keeps track of
> every coq version since 8.6. I use it to test my coquille plugin on
> every coq version that exists, but I'm sure there are other use cases
> :)
>

Nice! Noted. Thank you Julien :)

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

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

[Ludovic Courtès]

Hi!

Julien Lepiller <julien@lepiller.eu> skribis:

> I forgot to metion I have a small channel at
> https://framagit.org/tyreunom/guix-coq-channel that keeps track of
> every coq version since 8.6. I use it to test my coquille plugin on
> every coq version that exists, but I'm sure there are other use cases
> :)

That’s an interesting kind of channel that’d be worth promoting (I think
many people have similar needs for their CI.)  If you feel like writing
a blog post over the holidays…  ;-)

It’s also a very concrete item that’s directly useful to formal methods
people, a good way to create ties.

Ludo’.

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

[Brett Gilio]

Ludovic Courtès <ludo@gnu.org> writes:

> Hi!
>
> Julien Lepiller <julien@lepiller.eu> skribis:
>
>> I forgot to metion I have a small channel at
>> https://framagit.org/tyreunom/guix-coq-channel that keeps track of
>> every coq version since 8.6. I use it to test my coquille plugin on
>> every coq version that exists, but I'm sure there are other use cases
>> :)
>
> That’s an interesting kind of channel that’d be worth promoting (I think
> many people have similar needs for their CI.)  If you feel like writing
> a blog post over the holidays…  ;-)
>
> It’s also a very concrete item that’s directly useful to formal methods
> people, a good way to create ties.

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.

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?

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>

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

[Ludovic Courtès]

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!

> 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!

Thanks,
Ludo’.

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

[Brett Gilio]

Ludovic Courtès <ludo@gnu.org> writes:

> 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!

That is, of course, reasonable that we should pass this along for a
community decision among the maintainers. Though, I do wonder a bit
about the HPC project in its decision to host its domain on *.guix.info
and use the Gitlab instance instead of Savannah for developing the haunt
page? I am making an assumption it is for historical reasons, rather
than it being intentionally to distance itself from our relationship
with the GNU project, but I would like to know the story behind this
decision.

I am personally not partial to either domain: fm.guix.info or
fm.guix.gnu.org. I just wonder about how that original decision came
about :).

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>

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

[Ludovic Courtès]

Hello,

Brett Gilio <brettg@gnu.org> skribis:

> Ludovic Courtès <ludo@gnu.org> writes:
>
>> 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!
>
> That is, of course, reasonable that we should pass this along for a
> community decision among the maintainers. Though, I do wonder a bit
> about the HPC project in its decision to host its domain on *.guix.info
> and use the Gitlab instance instead of Savannah for developing the haunt
> page? I am making an assumption it is for historical reasons, rather
> than it being intentionally to distance itself from our relationship
> with the GNU project, but I would like to know the story behind this
> decision.

Guix-HPC is “institutional”, that’s part of the reason behind this.
Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
Also, <https://gitlab.inria.fr/guix-hpc/guix-hpc> is a channel developed
by colleagues at Inria, so it’s more convenient to have it there.

Ludo’.

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

[Brett Gilio]

Dec 30, 2019 3:34:22 PM Ludovic Courtès :

> Guix-HPC is “institutional”, that’s part of the reason behind this.
> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
> Also, is a channel developed
> by colleagues at Inria, so it’s more convenient to have it there.


Hey Ludo, thanks for the explanation.

It makes sense why Guix-HPC lives somewhere else. Given this, what do you propose for initiating the conversation on where the formal methods haunt page should live with the other maintainers? I personally think the repository should live on Savannah, but the address needs to be discussed.

Any other maintainers reading this, please feel free to weigh in.


-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>

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

[Ludovic Courtès]

Hello!

(Cc: maintainers.)

Brett Gilio <brettg@gnu.org> skribis:

> Dec 30, 2019 3:34:22 PM Ludovic Courtès :
>
>> Guix-HPC is “institutional”, that’s part of the reason behind this.
>> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
>> Also, is a channel developed
>> by colleagues at Inria, so it’s more convenient to have it there.
>
>
> Hey Ludo, thanks for the explanation.
>
> It makes sense why Guix-HPC lives somewhere else. Given this, what do you propose for initiating the conversation on where the formal methods haunt page should live with the other maintainers? I personally think the repository should live on Savannah, but the address needs to be discussed.

It’s fine to host the repo on Savannah: we can ask for a new repo under
the Guix umbrella, the downside being that access control will be the
same as for the other repos (we can only grant access to all the repos
or none of them.)  If you plan to open it more to formal methods people
that do not yet contribute to Guix, it might be easier to use a separate
repo.  You tell us!

As for the domain name: I think it would be fine to use
formal-methods.guix.gnu.org as long as the web site follows GNU and Guix
policy, which mostly means referring only to free software, avoiding the
phrase “open source” to describe it, and probably avoiding institution
logos and such (I don’t think there’s any written policy but I would
personally find it out of place on gnu.org.)  Anyway, the two of you are
webmasters so you probably know this better than I do.  IOW, if you want
to flatter your employers and labs, you might want to opt for a separate
web site.  :-)

Maintainers, what do you think?

Anyway, step #1 is to get a web page ready.  :-)

Ludo’.

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

[Amin Bandali]

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

Hi Ludo’, all,

Ludovic Courtès <ludo@gnu.org> writes:

> Hello!
>
> (Cc: maintainers.)
>
> Brett Gilio <brettg@gnu.org> skribis:
>
>> Dec 30, 2019 3:34:22 PM Ludovic Courtès :
>>
>>> Guix-HPC is “institutional”, that’s part of the reason behind this.
>>> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
>>> Also, is a channel developed
>>> by colleagues at Inria, so it’s more convenient to have it there.
>>
>>
>> Hey Ludo, thanks for the explanation.
>>
>> It makes sense why Guix-HPC lives somewhere else. Given this, what
>> do you propose for initiating the conversation on where the formal
>> methods haunt page should live with the other maintainers? I
>> personally think the repository should live on Savannah, but the
>> address needs to be discussed.
>
> It’s fine to host the repo on Savannah: we can ask for a new repo under
> the Guix umbrella, the downside being that access control will be the
> same as for the other repos (we can only grant access to all the repos
> or none of them.)  If you plan to open it more to formal methods people
> that do not yet contribute to Guix, it might be easier to use a separate
> repo.  You tell us!
>

Right.  Thinking about this, as I see it right now I think our use cases
for repos fall roughly into two categories:

- Closely Guix-related or small standalone things: this could be things
  like the Haunt sources for our site, or a Guix channel for additional
  package definitions, or anything closely related to Guix and/or small
  enough to fit under the Guix umbrella just fine.  For these, we should
  be able to get by with a very small number of repos in the short and
  long term.  Initially, we will only have one such repository, say,
  guix/guix-fm.git or guix/formal-methods.git, with its purpose being
  mainly to keep the sources for the site.

  For these repos we’ll happily accept patches from folks who aren’t
  Guix contributors via mailing list.  And I’d imagine once they have
  contributed enough patches, we could work out getting them commit
  access, especially if their gathered knowledge/experience extends to
  Guix directly (e.g. in form of familiarity with package definitions
  and writing them).

- Larger projects or ones that don’t quite fit the scope of Guix: for
  these, we might indeed consider registering separate Savannah projects
  rather than putting them under the Guix project.  I think the proposed
  bootstrapping ML compiler could be an example of such project.

All that said, I do wish Savannah supported finer access control at the
project level.  I just asked a fellow Savannah hacker for his opinion on
whether implementing that would be possible and feasible with the
current underlying infrastructure in mind.

>
> As for the domain name: I think it would be fine to use
> formal-methods.guix.gnu.org as long as the web site follows GNU and Guix
> policy, which mostly means referring only to free software, avoiding the
> phrase “open source” to describe it, and probably avoiding institution
> logos and such (I don’t think there’s any written policy but I would
> personally find it out of place on gnu.org.)  Anyway, the two of you are
> webmasters so you probably know this better than I do.  IOW, if you want
> to flatter your employers and labs, you might want to opt for a separate
> web site.  :-)
>

Most certainly; I wouldn’t expect anything less. :-)

As for institution logos, agreed.  If it ever comes such time that we
absolutely “have to” consider that, I’ll be sure to check with you and
the other Guix maintainers, fellow GNU webmasters, and of course rms.

As for the domain name, I think formal-methods.guix.gnu.org is a bit of
a mouthful to type or say on a regular basis, and I think an abbreviated
fm.guix.gnu.org would be more convenient; à la ci.guix.gnu.org.  For
what it’s worth, I’ve seen the FM abbreviation for Formal Methods used
fairly commonly around the community.

Lastly, I think it would be nice to have a guix-fm@gnu.org address for
Guix-FM.  Rather than a full-fledged Mailman list, I think a simple
alias, like with guix-hpc@gnu.org, will suffice.  Thoughts?

>
> Maintainers, what do you think?
>
> Anyway, step #1 is to get a web page ready.  :-)
>
> Ludo’.

I’ll work on putting one together over the next couple of days. :-)

Best,
amin

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 857 bytes --]

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

[Ludovic Courtès]

Hi Amin & Brett,

Amin Bandali <bandali@gnu.org> skribis:

>> It’s fine to host the repo on Savannah: we can ask for a new repo under
>> the Guix umbrella, the downside being that access control will be the
>> same as for the other repos (we can only grant access to all the repos
>> or none of them.)  If you plan to open it more to formal methods people
>> that do not yet contribute to Guix, it might be easier to use a separate
>> repo.  You tell us!
>>
>
> Right.  Thinking about this, as I see it right now I think our use cases
> for repos fall roughly into two categories:
>
> - Closely Guix-related or small standalone things: this could be things
>   like the Haunt sources for our site, or a Guix channel for additional
>   package definitions, or anything closely related to Guix and/or small
>   enough to fit under the Guix umbrella just fine.  For these, we should
>   be able to get by with a very small number of repos in the short and
>   long term.  Initially, we will only have one such repository, say,
>   guix/guix-fm.git or guix/formal-methods.git, with its purpose being
>   mainly to keep the sources for the site.
>
>   For these repos we’ll happily accept patches from folks who aren’t
>   Guix contributors via mailing list.  And I’d imagine once they have
>   contributed enough patches, we could work out getting them commit
>   access, especially if their gathered knowledge/experience extends to
>   Guix directly (e.g. in form of familiarity with package definitions
>   and writing them).

Sounds good to me.

> - Larger projects or ones that don’t quite fit the scope of Guix: for
>   these, we might indeed consider registering separate Savannah projects
>   rather than putting them under the Guix project.  I think the proposed
>   bootstrapping ML compiler could be an example of such project.

Yes.

> All that said, I do wish Savannah supported finer access control at the
> project level.  I just asked a fellow Savannah hacker for his opinion on
> whether implementing that would be possible and feasible with the
> current underlying infrastructure in mind.

I suppose it would be hard and not necessarily advisable given that
Savane is no longer actively developed, AIUI.

>> As for the domain name: I think it would be fine to use
>> formal-methods.guix.gnu.org as long as the web site follows GNU and Guix
>> policy, which mostly means referring only to free software, avoiding the
>> phrase “open source” to describe it, and probably avoiding institution
>> logos and such (I don’t think there’s any written policy but I would
>> personally find it out of place on gnu.org.)  Anyway, the two of you are
>> webmasters so you probably know this better than I do.  IOW, if you want
>> to flatter your employers and labs, you might want to opt for a separate
>> web site.  :-)
>>
>
> Most certainly; I wouldn’t expect anything less. :-)
>
> As for institution logos, agreed.  If it ever comes such time that we
> absolutely “have to” consider that, I’ll be sure to check with you and
> the other Guix maintainers, fellow GNU webmasters, and of course rms.

Sure, sounds good to me!  (Note that rms doesn’t have a say here, though.)

> As for the domain name, I think formal-methods.guix.gnu.org is a bit of
> a mouthful to type or say on a regular basis, and I think an abbreviated
> fm.guix.gnu.org would be more convenient; à la ci.guix.gnu.org.  For
> what it’s worth, I’ve seen the FM abbreviation for Formal Methods used
> fairly commonly around the community.

Alright, I like expressive phrases like ‘call-with-current-continuation’
but I’m fine with “fm” nonetheless.  ;-)

> Lastly, I think it would be nice to have a guix-fm@gnu.org address for
> Guix-FM.  Rather than a full-fledged Mailman list, I think a simple
> alias, like with guix-hpc@gnu.org, will suffice.  Thoughts?

Yeah, I guess a simple alias is enough for things that don’t fit on
guix-devel (guix-hpc@gnu.org is very low traffic, mostly for when one
needs to reach out to the usual HPC suspects.)

Let us know when you have a web page ready.  Then you’re welcome to send
a patch against maintenance.git for ‘bayfront.scm’ (DNS config and
probably web site as well.)

Thanks!

Ludo’.

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

[Maxim Cournoyer]

Hello,

Ludovic Courtès <ludo@gnu.org> writes:

> Hello!
>
> (Cc: maintainers.)
>
> Brett Gilio <brettg@gnu.org> skribis:
>
>> Dec 30, 2019 3:34:22 PM Ludovic Courtès :
>>
>>> Guix-HPC is “institutional”, that’s part of the reason behind this.
>>> Regarding gitlab.inria.fr, that’s because it used to be hosted at Inria.
>>> Also, is a channel developed
>>> by colleagues at Inria, so it’s more convenient to have it there.
>>
>>
>> Hey Ludo, thanks for the explanation.
>>
>> It makes sense why Guix-HPC lives somewhere else. Given this, what
>> do you propose for initiating the conversation on where the formal
>> methods haunt page should live with the other maintainers? I
>> personally think the repository should live on Savannah, but the
>> address needs to be discussed.
>
> It’s fine to host the repo on Savannah: we can ask for a new repo under
> the Guix umbrella, the downside being that access control will be the
> same as for the other repos (we can only grant access to all the repos
> or none of them.)  If you plan to open it more to formal methods people
> that do not yet contribute to Guix, it might be easier to use a separate
> repo.  You tell us!
>
> As for the domain name: I think it would be fine to use
> formal-methods.guix.gnu.org as long as the web site follows GNU and Guix
> policy, which mostly means referring only to free software, avoiding the
> phrase “open source” to describe it, and probably avoiding institution
> logos and such (I don’t think there’s any written policy but I would
> personally find it out of place on gnu.org.)  Anyway, the two of you are
> webmasters so you probably know this better than I do.  IOW, if you want
> to flatter your employers and labs, you might want to opt for a separate
> web site.  :-)
>
> Maintainers, what do you think?

I haven't followed the discussion of a formal methods work group
associated with Guix as closely as I should have, but I'm thrilled that
such an initiative is taking off!

> Anyway, step #1 is to get a web page ready.  :-)

Agreed.

Maxim

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

[Amin Bandali]

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

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: signature.asc --]
[-- Type: application/pgp-signature, Size: 857 bytes --]

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

[Vicente Eduardo]

[-- 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 --]

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

[Jan Nieuwenhuizen]

Vicente Eduardo writes:

Hi Vincente,

> 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.

What is "a C compiler for Scheme"?  We are working on a C compiler
written in Scheme, MesCC which is based on Nyacc; but that's not what
you propose to do?

Greetings,
janneke

-- 
Jan Nieuwenhuizen <janneke@gnu.org> | GNU LilyPond http://lilypond.org
Freelance IT http://JoyofSource.com | Avatar® http://AvatarAcademy.com

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

[Brett Gilio]

Julien Lepiller <julien@lepiller.eu> writes:

> OCaml stuff can easily be imported with guix import opam. I know coq
> packages use a separate opam repository, so it would be nice if the
> importer could take an optional parameter to indicate a custom opam
> repository url. I'm not sure the coq repo is converted to opam 2 yet
> though.

To my knowledge the Coq repo is not compliant with OPAM 2 quite
yet. Maybe this has changed since I last checked, but I would be more
than happy to ask upstream if this is still the case. I think working on
an importer for those modified OPAM->Coq packages would be a fantastic
start to that problem.

> I can see the benefits of formal methods and benefits of guix, but
> what does guix provide or could provide to formal method people
> specifically? Is it "only" the nice guarantees it gives to any
> programer, or is there something else? Maybe the question is why does
> it matter more to fm people than to other programmers?

I think it is a combination of what every other programmer is offered,
and the possibilities offered by what bootstrapping has to offer for
creating a machine from "nothing". There is still a lot of unknowns
here, but I speculate that there is definitely more to be found as the
concept progresses. I think your question is valid, and should likely be
a central thesis to the working group; "What does Guix offer to the
formal methods community that it could specifically benefit from?"

> I think we're still a small community, so we can continue talking
> about it on the main channel. We're trying to avoid dividing
> information, that's why we allow any language on tge channel, instead
> of having separate chans for each language. We also always hear about
> bootstrapping or the hpc effort on the main channel. Let's talk about
> fm :). You can count me in.

Agreed, lets not separate the community. Keep the communication
integrated. Though, I wonder if maybe I could draft an article for the
Guix website blog; or maybe we could organize our goals somewhere? I am
not quite sure what the best option here is. For example, one of the
goals is a possible bootstrapping compiler for ML that I mentioned
before, that would be dedicated to the GNU project in a similar fashion
to Jan's GNU Mes (which, thank you Jan for the supportive
messages). Combine this on maybe working out a bootstrap for OCaml,
creating an importer for Coq, working on some more programming
research-related questions in the context of Guix and suddenly we have
ourselves a trifecta of big questions that need to be articulated
_somewhere_ so we can retain some scope. Maybe Guix needs a wiki similar
to the wishlist, but dedicated to working groups? I really have no
idea. Just something, somewhere to centralize our goals.

Regardless, thank you for the supportive voice Julien. I am glad to have
your support.

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

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

[zimoun]

Hi,

I am not a Programming Language Theory guy so I speak as a pure noob. :-)
Well, I am working in University Paris 7 Diderot doing some scientific
computing.


On Mon, 16 Dec 2019 at 02:00, Brett Gilio <brettg@posteo.net> wrote:

> so this could be more of a chance to see bigger institutions begin to
> adopt Guix for their research work.

IMHO, today the "win" is not about bootstrapping because it is
strongly language dependent but this "win" offered by Guix is about
the time-traveling reproducibility tools: today the key point in
scientific research (IMHO).
And yes, the reproducibility over the time means bootstrappability.
But it is each scientific community that must take care of its
outputs.

The wider adoption could come from features as "time-machine",
available packages (channels for the not GNU compliant), easy to
distribute, to reproduce, be able to search in all the packages over
all the Guix history, etc.

And what I see as a blocking wider adoption by the Researcher around
me is: Mac. A lot of them just use Mac, I mean they develop daily on
MacOS and then once it is ready run on linux HPC clusters.

I know the article by Ludo and Ricardo. :-) And I strongly agree.
From my point of view, the only way to attract more researchers is to
have an half-baked Guix working on Mac, IMHO.


> -- 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.]

It is a ambitious research project. Woow! Nice!! :-)

CakeML [1] claims to be a subset of Standard ML and to be
boostrappable. I do not know enough to have an relevant opinion.

[1] https://cakeml.org/

What is the status of OCaml about boostrappability?


> -- Begin giving talks on the benefits of GNU Guix at conferences around
>    Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

Yes, let spread the world! :-)

And IMO a good start is to show in scientific communities why
boostrappability matters.

For example, the papers which were OK in [2] (2015), are they still OK
in 2019? I bet that a lot of big binary blobs have disappear since
then.

[2] http://repeatability.cs.arizona.edu/



All the best,
simon

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

[Julien Lepiller]

Le 16 décembre 2019 20:46:28 GMT+01:00, zimoun <zimon.toutoune@gmail.com> a écrit :
>Hi,
>
>I am not a Programming Language Theory guy so I speak as a pure noob.
>:-)
>Well, I am working in University Paris 7 Diderot doing some scientific
>computing.
>
>
>On Mon, 16 Dec 2019 at 02:00, Brett Gilio <brettg@posteo.net> wrote:
>
>> so this could be more of a chance to see bigger institutions begin to
>> adopt Guix for their research work.
>
>IMHO, today the "win" is not about bootstrapping because it is
>strongly language dependent but this "win" offered by Guix is about
>the time-traveling reproducibility tools: today the key point in
>scientific research (IMHO).
>And yes, the reproducibility over the time means bootstrappability.
>But it is each scientific community that must take care of its
>outputs.
>
>The wider adoption could come from features as "time-machine",
>available packages (channels for the not GNU compliant), easy to
>distribute, to reproduce, be able to search in all the packages over
>all the Guix history, etc.
>
>And what I see as a blocking wider adoption by the Researcher around
>me is: Mac. A lot of them just use Mac, I mean they develop daily on
>MacOS and then once it is ready run on linux HPC clusters.
>
>I know the article by Ludo and Ricardo. :-) And I strongly agree.
From my point of view, the only way to attract more researchers is to
>have an half-baked Guix working on Mac, IMHO.
>
>
>> -- 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.]
>
>It is a ambitious research project. Woow! Nice!! :-)
>
>CakeML [1] claims to be a subset of Standard ML and to be
>boostrappable. I do not know enough to have an relevant opinion.
>
>[1] https://cakeml.org/
>
>What is the status of OCaml about boostrappability?

I'm afraid OCaml is not bootstrappable. It uses a bytecode version of itself (using a bootstrapped bytecode interpreter written in C) to build itself. Fortunately this situation is being worked on by a phd student of Xavier Leroy (and nixOS user) :).

The plan is to write a compiler in C or Scheme (it currently exists, but is written in OCaml) for "miniML" a small subset of the OCaml language. Then, there is already an interpreter in miniML able to interpret the OCaml compiler compiling itself. Once the miniML compiler is bootstrapped, we will have a path from C to OCaml :)

>
>
>> -- Begin giving talks on the benefits of GNU Guix at conferences
>around
>>    Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.
>
>Yes, let spread the world! :-)
>
>And IMO a good start is to show in scientific communities why
>boostrappability matters.
>
>For example, the papers which were OK in [2] (2015), are they still OK
>in 2019? I bet that a lot of big binary blobs have disappear since
>then.
>
>[2] http://repeatability.cs.arizona.edu/
>
>
>
>All the best,
>simon

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

[Brett Gilio]

Julien Lepiller <julien@lepiller.eu> writes:

> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of
> itself (using a bootstrapped bytecode interpreter written in C) to
> build itself. Fortunately this situation is being worked on by a phd
> student of Xavier Leroy (and nixOS user) :).
>
> The plan is to write a compiler in C or Scheme (it currently exists,
> but is written in OCaml) for "miniML" a small subset of the OCaml
> language. Then, there is already an interpreter in miniML able to
> interpret the OCaml compiler compiling itself. Once the miniML
> compiler is bootstrapped, we will have a path from C to OCaml :)

I did not know of this project. Thank you for telling me!

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

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

[Ludovic Courtès]

Hi!

Julien Lepiller <julien@lepiller.eu> skribis:

> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of
> itself (using a bootstrapped bytecode interpreter written in C) to
> build itself. Fortunately this situation is being worked on by a phd
> student of Xavier Leroy (and nixOS user) :).
>
> The plan is to write a compiler in C or Scheme (it currently exists,
> but is written in OCaml) for "miniML" a small subset of the OCaml
> language. Then, there is already an interpreter in miniML able to
> interpret the OCaml compiler compiling itself. Once the miniML
> compiler is bootstrapped, we will have a path from C to OCaml :)

Do you have pointers to this work?

Hannes of MirageOS also mentioned it at the Reproducible Builds Summit.
It sounds exciting!

Ludo’.

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

[Brett Gilio]

Ludovic Courtès <ludo@gnu.org> writes:

> Hi!
>
> Julien Lepiller <julien@lepiller.eu> skribis:
>
>> I'm afraid OCaml is not bootstrappable. It uses a bytecode version of
>> itself (using a bootstrapped bytecode interpreter written in C) to
>> build itself. Fortunately this situation is being worked on by a phd
>> student of Xavier Leroy (and nixOS user) :).
>>
>> The plan is to write a compiler in C or Scheme (it currently exists,
>> but is written in OCaml) for "miniML" a small subset of the OCaml
>> language. Then, there is already an interpreter in miniML able to
>> interpret the OCaml compiler compiling itself. Once the miniML
>> compiler is bootstrapped, we will have a path from C to OCaml :)
>
> Do you have pointers to this work?
>
> Hannes of MirageOS also mentioned it at the Reproducible Builds Summit.
> It sounds exciting!
>
> Ludo’.
>

I am also interested in this. MirageOS has a long lineage of making
sensible decisions in their development aside from just designing their
unikernel. So i'd really like to see if this becomes a possible bridge
from C or Scheme to a bootstrappable OCaml. For what I wonder, I think
this is something a formal methods community in Guix would be able to
contribute to so we see to it that GNU Guix has a good foundation for
making OCaml properly bootstrappable.

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>

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

[Brett Gilio]

zimoun <zimon.toutoune@gmail.com> writes:

> Hi,
>
> I am not a Programming Language Theory guy so I speak as a pure noob. :-)
> Well, I am working in University Paris 7 Diderot doing some scientific
> computing.

We are all noobs of formal methods next to Vladimir Voevodsky, and
Grothendiek. ;)

>> so this could be more of a chance to see bigger institutions begin to
>> adopt Guix for their research work.
>
> IMHO, today the "win" is not about bootstrapping because it is
> strongly language dependent but this "win" offered by Guix is about
> the time-traveling reproducibility tools: today the key point in
> scientific research (IMHO).
> And yes, the reproducibility over the time means bootstrappability.
> But it is each scientific community that must take care of its
> outputs.
>
> The wider adoption could come from features as "time-machine",
> available packages (channels for the not GNU compliant), easy to
> distribute, to reproduce, be able to search in all the packages over
> all the Guix history, etc.

Undoubtedly the formal methods community, just as with all other
communities of scientific research stands to benefit from the
time-machine! No question about that. I would be intrigued to see in
what ways we can push that paradigm to its limits. Formal methods is
notorious for finding novel ways to bring change to our systems of
abstraction, and challenge our notions of things like "safety". So maybe
the time-machine could still stand to benefit from improvement, and maybe the formal
methods community by using it will find out ways to do that. Purely
speculation, here.

>> -- 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.]
>
> It is a ambitious research project. Woow! Nice!! :-)
>
> CakeML [1] claims to be a subset of Standard ML and to be
> boostrappable. I do not know enough to have an relevant opinion.
>
> [1] https://cakeml.org/

I am quite familiar with CakeML, and I draw a lot of inspiration with
the things they are managing to do as a subset implementation of ML. I
think it would be interesting to see where a bootstrapping compiler
could go if it were fledged out into a full implementation for the GNU
project, filling a dual-role. Again, just proposing some ideas. :)

> What is the status of OCaml about boostrappability?

Julien answered this already, but there is a gap here.

> Yes, let spread the world! :-)
>
> And IMO a good start is to show in scientific communities why
> boostrappability matters.
>
> For example, the papers which were OK in [2] (2015), are they still OK
> in 2019? I bet that a lot of big binary blobs have disappear since
> then.
>
> [2] http://repeatability.cs.arizona.edu/
>
>
>
> All the best,
> simon

Simon, I am glad to have your support here! Please engage with us more
as more details come. You may be a "noob" (self-reported), but it is
noobs who provide us the most valuable information often times.

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

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

[Jack Hill]

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

Greetings,

On Sun, 15 Dec 2019, Brett Gilio wrote:

> Hello Guix!
>
> This is going to be a rather lengthy email proposing a new working group
> (if that is indeed the proper name for this) in the GNU Guix
> project. Just as there are other "working groups" for GNOME packages,
> bootstrapping Rust & JVM, and bootstrapping the entirely of the GNU
> Corelibs (GNU Mes) in Guix, I am proposing a new working group based on
> the synthesis of two fundamentally and mutually agreeable concepts.
>
> This is a continuation of the discussion proposed by Amin Bandali, Leo
> Prikler, and I from the #guix Freenode IRC. All three of us are either
> students of formal methods in mathematics and computer science, users of
> proof assistants, or interested in category theory and type theory. As
> such as noticed and wondered what kind of community there is for formal
> methods in GNU Guix, and by extension what kind of benefits GNU Guix has
> to offer the formal methods community which is providing some of the
> most rigorous research in computing methods to date.

[…]

> Having Guix and the Formal Methods community aligned would mean a great
> deal of power for both camps! Just as we see with the Software Heritage
> project and Guix, for providing historical and state-consistent
> reproducible environments for software testing we and correspond to
> formal methods much of the same guarantees of deterministic
> computational states, modeling, and reasoning in software correctness.

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.

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.

[…]

> 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

> -- Begin adding more projects that are important works in the formal
>   methods community. We have Coq, Idris, and Agda, but there is a lot of work
>   to be done on keeping these projects not only up-to-date but also
>   adding subprojects that use these toolchains. For example: C Minor,
>   Metamath, Ynot, Formally verified Featherweight Scala, RustBelt,
>   RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of
>   various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid
>   Haskell, extensions to Z3, and tons more!

I would love to have more tools like these in Guix, so that we can use 
Guix's repoducibility guarantees to have them as part of the historical 
record.

> All of this seems really nice and impressive, but what is it without
> getting some feedback from the community? I'd _really_ love to hear your
> thoughts, experiences, and more on this working group idea and other
> working groups to avoid pitfalls. Maybe we should have a secondary
> #guix-fm channel on IRC? There is definitely a lot of work to be done
> here, and we will need some form of organizational structure to keep the
> work consistent and neatly integrated with the goals and purposes of GNU
> Guix.
>
> I hope to hear from the community.

Thanks for proposing the idea!

All the best,
Jack

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

[John Soo]

Hey this is great!

I’m a hobbyist too but I’m glad to see a formal methods community in Guix!  I’ll be following. 

- John

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

[Brett Gilio]

John Soo <jsoo1@asu.edu> writes:

> Hey this is great!
>
> I’m a hobbyist too but I’m glad to see a formal methods community in Guix!  I’ll be following. 
>
> - John

Thank you for voicing your support John! Glad to see there is an
inspiring community following for this idea.

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

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

[Brett Gilio]

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/>

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

[Amin Bandali]

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

Hello Guix!

Thank you Brett for taking initiative and putting this awesome proposal
together on all our behalves, and to everyone else for chiming in and
expressing your interest and support!

To share some of my (scattered) thoughts on this, as a researcher I
think reproducible and verifiable research is a crucially important
topic, yet traditionally and often a neglected one.  Throughout my
graduate studies, too many times I stumbled on papers with interesting
claims that I sadly could not reproduce or easily verify for myself.
And I think this is especially ironic and painful for those of us doing
research in formal methods, computing science, and software engineering;
and is where projects like GNU Guix with their awesome efforts in
reproducibility could act as role models and show what's possible.

For instance, for better or worse many of the tools I have worked with
over the last few years are primarily implemented in Java, often in form
Eclipse plugins.  Suffice to say that release management, bundling, and
distribution practices of most of these tools leave a lot to be desired.
As part of the Formal Methods in GNU Guix Working Group, I'd love for us
to try and get in touch with the developers of these tools and offer to
work with them to challenge and improve the status quo, resulting
ultimately in more readily and easily accessible tools, greatly useful
for verifying and reproducing existing literature.

As Brett and I alluded to, there's a large variety of tasks in all
shapes and sizes that could use your help, from more "researchy" work
like writing a bootstrapping SML '97 compiler, or exploring synthesis
and verification for GNU Guile and GNU Guix, to less researchy ones like
packaging (even more) formal methods-related software and helping their
developers improve their release and package qualities.

We would love to hear more from you about this in trying to gradually
put together actionable plans.  If you'd like to chat with us, please
come say hi to us in the #guix IRC channel on freenode.  My nick there
is bandali, and Brett is brettgilio.

Best,
amin

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 857 bytes --]

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

[Brett Gilio]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Amin Bandali <bandali@gnu.org> writes:

> Hello Guix!
>
> Thank you Brett for taking initiative and putting this awesome proposal
> together on all our behalves, and to everyone else for chiming in and
> expressing your interest and support!
>
> To share some of my (scattered) thoughts on this, as a researcher I
> think reproducible and verifiable research is a crucially important
> topic, yet traditionally and often a neglected one.  Throughout my
> graduate studies, too many times I stumbled on papers with interesting
> claims that I sadly could not reproduce or easily verify for myself.
> And I think this is especially ironic and painful for those of us doing
> research in formal methods, computing science, and software engineering;
> and is where projects like GNU Guix with their awesome efforts in
> reproducibility could act as role models and show what's possible.
>
> For instance, for better or worse many of the tools I have worked with
> over the last few years are primarily implemented in Java, often in form
> Eclipse plugins.  Suffice to say that release management, bundling, and
> distribution practices of most of these tools leave a lot to be desired.
> As part of the Formal Methods in GNU Guix Working Group, I'd love for us
> to try and get in touch with the developers of these tools and offer to
> work with them to challenge and improve the status quo, resulting
> ultimately in more readily and easily accessible tools, greatly useful
> for verifying and reproducing existing literature.
>
> As Brett and I alluded to, there's a large variety of tasks in all
> shapes and sizes that could use your help, from more "researchy" work
> like writing a bootstrapping SML '97 compiler, or exploring synthesis
> and verification for GNU Guile and GNU Guix, to less researchy ones like
> packaging (even more) formal methods-related software and helping their
> developers improve their release and package qualities.
>
> We would love to hear more from you about this in trying to gradually
> put together actionable plans.  If you'd like to chat with us, please
> come say hi to us in the #guix IRC channel on freenode.  My nick there
> is bandali, and Brett is brettgilio.
>
> Best,
> amin
>

Hello, everybody!

Thank you, Amin for your substantial contribution in this last email. I
am 100% in agreement with your assessment, and there is definitely a
plethora of work to be done here!

To kick-start the project I am wanting to make some suggestions, mostly
pertaining to the organization and up-keep of the working group.

1. Just as the bootstrappability and guix-hpc projects have their own
websites documenting their efforts, I think it would be nice to have
https://fm.guix.gnu.org/ which would host a Haunt-generated
website. This website would be hosted in the Savannah project structure
for GNU Guix. This would document who is active in the coordination and
oversight of this working group, and would express a clear and mutual
relationship with the GNU Guix / Guix System project.

2. Perhaps we should adopt a particular tag for the Guix Debbugs
tracker, so as to be able to clearly delineate that this particular
patch or bug is in relation with the formal methods working
group. Maybe something like [FM].

3. It was suggested that maybe a #guix-fm IRC channel might be useful,
but we have had a mixed bag of opinions on this. I personally think that
keeping everything together is the better solution, but I'd still like
to hear acceptance or criticism of this idea.

4. A lot of documenting working group milestones (Working on a Coq
sub-importer for OPAM, writing a bootstrapping compiler for SML97,
doing regular packaging duties for formal methods projects,
communicating upstream about distribution package quality, and perhaps
even trying to do formal methods work via synthesis in GNU Guile / GNU
Guix would be likely best expressed on the mailing list, and the
https://fm.guix.gnu.org/ website, but this likely rests in the hands of
the GNU Guix maintainers, of which I am not.

5. Additionally, maybe making an introductory post on the
https://guix.gnu.org/ blog about the preliminary goals of the working
group, after having our own subdomain established, would be a good way
to attract some attention to the project by distributing links to it on
HackerNews, Reddit, and Formal Methods/Functional Programming-related
mailing lists.

Anyways, I am going to CC Ludo' in this message to see what he might
have to say about these proposals.

Thanks for everybody who has chimed in!

- -- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCAAdFiEE38DH957mDKeuVV4ZZyJDxKA/Du4FAl3+sdcACgkQZyJDxKA/
Du7YyhAAqEZqbOO1W37xKvd8EztAp/dYJ1Q9Bt/mw9eH0Aj95lxkFQkl9Iq+Bvqa
DGPiVeyR7nOn/AtKdZMwrgz9xZXE43pQ1C8IV8+Jbssv9l3G2UQdzwIiP4YyFKum
Lj7kkNEKC5GZ9CpgMcSHGevmW+YpTcTIVOZWFve/4eera27Ds9RMgME8q8FaKKLt
CoYwi0JeHqUmlP+ZrYJ2KSPVyffxFZjW5W1SnrKoLtzp+w70j/E1m0kSr1SpPuZ2
sDwGK/gM3pQ8wHMxLwbP9MFU3S2lsqryr9Uiefca43He94KhrHOpq266nHH96FsF
GfgflhYZfCuhm6gL7iZg/3valjAFcF0JJS59CymQ32DI9zgTnexeGjd9NXjl9kf7
X6J5/CuWrra7IDJ8f5/iqnF5XjS132R6a5jIJz5BwPDag8mqDKA2xKtb16FkND/I
ZCcnI+EA8pXbh2awmNKoG0c6penPY5+falcCNJ/T2bn3KsXsk4JymwePYa38jYUr
GCauYGt6W3DfauAHJ+maNjxvtsWIGP5+gIbG/JViClSndT6zHOBinHGdFobz5AjN
fEdCx4kyoWo2rrmTrnWBuaDtNNPnuW0y8zx9qjQ9k9LXFAp1nyRJ46x1LVAhl+3U
uvHhAWiVNLuqreLEJPitZE3lebwt9r2m7/VpKQH7UL8CVA3ws/o=
=Y0Ml
-----END PGP SIGNATURE-----

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

[Ludovic Courtès]

Hi Brett,

Brett Gilio <brettg@gnu.org> skribis:

> 1. Just as the bootstrappability and guix-hpc projects have their own
> websites documenting their efforts, I think it would be nice to have
> https://fm.guix.gnu.org/ which would host a Haunt-generated
> website. This website would be hosted in the Savannah project structure
> for GNU Guix. This would document who is active in the coordination and
> oversight of this working group, and would express a clear and mutual
> relationship with the GNU Guix / Guix System project.

Like I wrote in another message, the only question will be the domain
name, but other than that it sounds great.

> 2. Perhaps we should adopt a particular tag for the Guix Debbugs
> tracker, so as to be able to clearly delineate that this particular
> patch or bug is in relation with the formal methods working
> group. Maybe something like [FM].

I’d say let’s figure it out when it becomes an issue.  :-)

> 3. It was suggested that maybe a #guix-fm IRC channel might be useful,
> but we have had a mixed bag of opinions on this. I personally think that
> keeping everything together is the better solution, but I'd still like
> to hear acceptance or criticism of this idea.

Keeping everything on #guix for now sounds like the right thing to me.

> 4. A lot of documenting working group milestones (Working on a Coq
> sub-importer for OPAM, writing a bootstrapping compiler for SML97,
> doing regular packaging duties for formal methods projects,
> communicating upstream about distribution package quality, and perhaps
> even trying to do formal methods work via synthesis in GNU Guile / GNU
> Guix would be likely best expressed on the mailing list, and the
> https://fm.guix.gnu.org/ website, but this likely rests in the hands of
> the GNU Guix maintainers, of which I am not.
>
> 5. Additionally, maybe making an introductory post on the
> https://guix.gnu.org/ blog about the preliminary goals of the working
> group, after having our own subdomain established, would be a good way
> to attract some attention to the project by distributing links to it on
> HackerNews, Reddit, and Formal Methods/Functional Programming-related
> mailing lists.

Sounds like a great plan to me!

Ludo’.

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

[Ludovic Courtès]

Hi!

Brett Gilio <brettg@posteo.net> skribis:

> Having Guix and the Formal Methods community aligned would mean a great
> deal of power for both camps! Just as we see with the Software Heritage
> project and Guix, for providing historical and state-consistent
> reproducible environments for software testing we and correspond to
> formal methods much of the same guarantees of deterministic
> computational states, modeling, and reasoning in software correctness.
>
> Amin, Leo, and I all likely agree that _some_ relationship here is good
> to be opened and explored! I know that there are some of us who come
> from institutions that have historical relationships to the proof
> assistant community, Caml, HOL (looking at you Ludo', though IIRC you
> are in a different working group at INRIA),
> so this could be more of a chance to see bigger institutions begin to
> adopt Guix for their research work.

For the record, I don’t work with the formal methods people at Inria,
but we chat occasionally, and I’d be happy to draw their attention to
this effort.  :-)

> 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.]

That’s sounds very ambitious, though it’s not like people here haven’t
been ambitious so far.  ;-)

Note that there’s an alternative tradition of theorem provers in Lisp
with ACL2, “The Little Prover”, etc.

> -- Begin adding more projects that are important works in the formal
>    methods community. We have Coq, Idris, and Agda, but there is a lot of work
>    to be done on keeping these projects not only up-to-date but also
>    adding subprojects that use these toolchains. For example: C Minor,
>    Metamath, Ynot, Formally verified Featherweight Scala, RustBelt,
>    RedPRL, NuPRL, JonPRL, HOL/Isabelle, F*, kreMLin, CakeML, tons of
>    various type checkers based on OCaml, Alloy, Frama-C, TLA+, Liquid
>    Haskell, extensions to Z3, and tons more!

+1

> -- Possibly begin formally verifying some of the behavior and
>    implementations of GNU Guix and GNU Guile. This is kind of an add-on
>    idea, but it struck our interest so why leave it out?

Put this way, it seems very broad.  One thing I’d like to have is (1)
Racket-style contracts, in particular for our record types, and (2)
Turnstile-style static type checking, again primarily for record types.

> -- Begin giving talks on the benefits of GNU Guix at conferences around
>    Homotopy Type Theory, Coq, Formal Verification, Deepspec, etc.

+1!

> All of this seems really nice and impressive, but what is it without
> getting some feedback from the community? I'd _really_ love to hear your
> thoughts, experiences, and more on this working group idea and other
> working groups to avoid pitfalls. Maybe we should have a secondary
> #guix-fm channel on IRC? There is definitely a lot of work to be done
> here, and we will need some form of organizational structure to keep the
> work consistent and neatly integrated with the goals and purposes of GNU
> Guix.

I agree with Julien that a separate IRC channel is unneeded at this
stage; as for the structure, I would start with a web page explaining
your areas of interests, similar to the Guix-HPC thing.

To me, an important goal is to create ties with formal methods people,
and to increase the bandwidth between us.  That can beget new ideas and
perspectives.

Then there are specific areas where we should be discussing: compiler
bootstrapping (what can OCaml, GHC, SMLNJ, etc. developers do to make
their compilers bootstrappable?), package management (how to turn OPAM,
etc. into functional package managers, or how to get language X to use
Guix instead of rolling its own?), development facilities (‘guix
environment’, channels like Julien’s Coq channel), and so on.

These things take time and we don’t necessarily have an idea what the
outcome should be, but it’s definitely worthwhile.

Thanks,
Ludo’.

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

[Brett Gilio]

Ludovic Courtès <ludo@gnu.org> writes:

> For the record, I don’t work with the formal methods people at Inria,
> but we chat occasionally, and I’d be happy to draw their attention to
> this effort.  :-)

I thought not, but I think this smells of potential for collaboration
maybe amongst a few there. I know some INRIA people from the Caml and
Coq community, so I think if they see a notification both internally and
externally of what is happening with this proposal (after we establish
it a bit more) it has the potential to get some attention.

> That’s sounds very ambitious, though it’s not like people here haven’t
> been ambitious so far.  ;-)

It is absolutely an ambitious task, and is definitely a daunting one to
try and make happen. I do have some experience with compiler
construction, but nothing quite to this extent. Amin and I have been
trying to establish connections with other people who might share this
goal, and from what we've received it is _this_ particular task of
making a bootstrapping compiler for ML that seems to be the most
attention-getting. There is definitely a need here, we realized. So, if
we are able to garner enough people to help make this task more
manageable then I say it is in the realm of possibility and will prove
useful for Guix.

> Note that there’s an alternative tradition of theorem provers in Lisp
> with ACL2, “The Little Prover”, etc.

I am familiar :). The Little Prover and the Little Typer are
foundational to my interest here. I have not considered ways to include
them, so food for thought!


> I agree with Julien that a separate IRC channel is unneeded at this
> stage; as for the structure, I would start with a web page explaining
> your areas of interests, similar to the Guix-HPC thing.
>
> To me, an important goal is to create ties with formal methods people,
> and to increase the bandwidth between us.  That can beget new ideas and
> perspectives.
>
> Then there are specific areas where we should be discussing: compiler
> bootstrapping (what can OCaml, GHC, SMLNJ, etc. developers do to make
> their compilers bootstrappable?), package management (how to turn OPAM,
> etc. into functional package managers, or how to get language X to use
> Guix instead of rolling its own?), development facilities (‘guix
> environment’, channels like Julien’s Coq channel), and so on.
>
> These things take time and we don’t necessarily have an idea what the
> outcome should be, but it’s definitely worthwhile.

Agreed! 100%. We have a lot of lateral connection making to do, and I
will help foster that any way I can. By the sound of it, Amin has
already been working with some of the Lean prover people on Zulip to see
what is possible for attracting some attention there. I will do my part
on this as well, and once we get an organizational page made for the
working group at whatever address it exists at, I think we will be able
to get some cross-pollination like we need. I definitely want to do this
the "right way".

Thank you Ludo for your help!

-- 
Brett M. Gilio
GNU Guix, Contributor | GNU Project, Webmaster
[DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
<brettg@gnu.org> <brettg@posteo.net>