unofficial mirror of guix-devel@gnu.org 
 help / color / mirror / code / Atom feed
* [Proposal] The Formal Methods in GNU Guix Working Group
@ 2019-12-16  0:59 Brett Gilio
  2019-12-16  8:47 ` Julien Lepiller
                   ` (4 more replies)
  0 siblings, 5 replies; 44+ messages in thread
From: Brett Gilio @ 2019-12-16  0:59 UTC (permalink / raw)
  To: guix-devel; +Cc: leo.prikler, bandali

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/

^ permalink raw reply	[flat|nested] 44+ messages in thread
* [Proposal] The Formal Methods in GNU Guix Working Group
@ 2020-01-23 19:17 Alexandru-Sergiu Marton
  0 siblings, 0 replies; 44+ messages in thread
From: Alexandru-Sergiu Marton @ 2020-01-23 19:17 UTC (permalink / raw)
  To: brettg, guix-devel

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

^ permalink raw reply	[flat|nested] 44+ messages in thread
* Re: [Proposal] The Formal Methods in GNU Guix Working Group
@ 2020-02-12 12:02 Orians, Jeremiah (DTMB)
  2020-02-12 14:16 ` zimoun
  0 siblings, 1 reply; 44+ messages in thread
From: Orians, Jeremiah (DTMB) @ 2020-02-12 12:02 UTC (permalink / raw)
  To: vic798@gmail.com; +Cc: guix-devel@gnu.org

> 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

^ permalink raw reply	[flat|nested] 44+ messages in thread

end of thread, other threads:[~2020-02-21 14:48 UTC | newest]

Thread overview: 44+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2019-12-16  0:59 [Proposal] The Formal Methods in GNU Guix Working Group Brett Gilio
2019-12-16  8:47 ` Julien Lepiller
2019-12-16  9:22   ` Julien Lepiller
2019-12-17  3:29     ` Brett Gilio
2019-12-27 18:56     ` Ludovic Courtès
2019-12-27 22:33       ` Brett Gilio
2019-12-27 23:37         ` Ludovic Courtès
2019-12-28  2:59           ` Brett Gilio
2019-12-30 21:34             ` Ludovic Courtès
2019-12-31 10:17               ` Brett Gilio
2020-01-02 22:11                 ` Ludovic Courtès
2020-01-03 23:49                   ` Amin Bandali
2020-01-15 21:59                     ` Ludovic Courtès
2020-01-13 19:27                   ` Maxim Cournoyer
2019-12-28  7:20           ` Amin Bandali
2019-12-28 11:28             ` Vicente Eduardo
2019-12-29  8:09               ` Jan Nieuwenhuizen
2019-12-17  3:27   ` Brett Gilio
2019-12-16 19:46 ` zimoun
2019-12-16 20:10   ` Julien Lepiller
2019-12-17  3:40     ` Brett Gilio
2019-12-27 23:56     ` Ludovic Courtès
2019-12-28  2:55       ` Brett Gilio
2019-12-17  3:38   ` Brett Gilio
2019-12-16 23:04 ` Jack Hill
2019-12-17  1:33   ` John Soo
2019-12-17  3:49     ` Brett Gilio
2019-12-17  3:48   ` Brett Gilio
2019-12-21  6:48 ` Amin Bandali
2019-12-21 23:59   ` Brett Gilio
2019-12-28  0:02     ` Ludovic Courtès
2019-12-27 23:54 ` Ludovic Courtès
2019-12-28  3:06   ` Brett Gilio
  -- strict thread matches above, loose matches on Subject: below --
2020-01-23 19:17 Alexandru-Sergiu Marton
2020-02-12 12:02 Orians, Jeremiah (DTMB)
2020-02-12 14:16 ` zimoun
2020-02-12 14:38   ` Svante Signell
2020-02-12 14:48     ` Jan Nieuwenhuizen
2020-02-12 20:59   ` Bengt Richter
2020-02-13 12:13     ` Orians, Jeremiah (DTMB)
2020-02-13 12:07   ` Orians, Jeremiah (DTMB)
2020-02-15 16:10     ` zimoun
2020-02-18 11:17       ` Orians, Jeremiah (DTMB)
2020-02-21 14:47         ` zimoun

Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/guix.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).