Dear Alexander, Many thanks for your reply and your encouragements. The point that you raised is very interesting and was partially done in Debian (they defined a wrapper around apt-get instead of refactoring it): http://manpages.ubuntu.com/manpages/zesty/man8/apt-cudf-get.8.html Part of their work was formalized in coq and implemented in OCaml. In our case, we don't have any mechanized formalization of our model (maybe in the future).
I too (and my colleagues) hope that someone on the team could have some time to look into our project. But maybe there are things we can do to help start a dialog, like: - reaching in other mailing lists - posting on a Gentoo forum - participating in a workshop/conference/other where we could directly meet and discuss with the community - or simply starting an informal discussion by email where instead of having to look into the Github repository, you could directly ask me Does anyone have suggestions on that topic? Again, many thanks. I really hope that with everyone's feedback, suggestions, and help, we could make something useful from this prototype. Michael Lienhardt PS: I forgot in my previous mail to talk about the other persons involved in this project: - Jacopo Mauro, Post-doc in UiO (Norway), developer of the solver backend - Simone Donetti, Engineer in Unito (Italy), he helped me perform some tests - Ferruccio Damiani (Unito), Einar Broch Johnsen and Ingrid Chieh Yu (UiO), our supervisors
