Hi Nik, thank you for the kind and informative reply. I will see what to do.
So far I've joined the slack. For what I've seen so far, Discourse may work as a good alternative, but I don't know exactly your requirements. Discourse forums can be both public and private, have roles, be by invite, and are organized around archivable topics. So far I've not found on the internet anyone complaining about the archiving function. I would consider it. My two cents right now. Thank you again Nik! All the bests, Christian Il giorno ven 11 gen 2019 alle ore 17:37 Nikhil Swamy <nsw...@microsoft.com> ha scritto: > Dear Christian, > > > > Thanks for your interest in F*! > > > > I respond to some of your questions quite broadly below. I’ll let others > respond further with more specifics. > > > > -Nik > > > > *From:* fstar-club <fstar-club-boun...@lists.gforge.inria.fr> *On Behalf > Of *Christian Nyumbayire via fstar-club > *Sent:* Wednesday, January 9, 2019 6:42 PM > *To:* fstar-club@lists.gforge.inria.fr > *Subject:* [fstar-club] Noob questions > > > > Hi, > I'm a programmer working in crypto (both cryptography and cryptocurrency). > I've learned about KreMLin from the Hacl slides and youtube video. I got > quite interested in FStar since then. I'm trying to learn more and figure > out how I could use it on a daily basis (if possible/advisable). So far I > can read the hacl mitls and I'm quite reassured that Meta FStar or things I > still don't grok properly are not generally used. My public code is mostly > in Rust. I have really a lot of questions but these ones are the most > pressing: > > 1. What is the best way to extend the fstar library? I was thinking > about I/O in particular.*[NS] *fsa > > *[NS] We are happy to consider pull requests for library improvements. > Please see CONTRIBUTIONS.md for some general guidelines.* > > *About IO in particular: there are many choices for how best to model it > with various tradeoffs. As a baseline, one can assume an effectful > operation and provide an implementation for it in whatever target language > you’re interested in running your program, e.g., OCaml, C etc.* > > 1. Is there any reason there is no stdin in kremlib, even as a channel? > 2. What is the proper way to extend kremlib? (I've seen the include) > 3. Anyone working on a builder to supplant the actual use of > Makefiles? E.g. in ocaml? Could be useful for a package manager in a second > phase. > > *[NS] No one is working on this, as far as I know. We rely heavily on F*’s > dependence analysis (fstar –dep) and Makefiles for builds currently. We are > not necessarily looking to remove our reliance on Make, but are open to > proposals. A package manager would be useful, but, as you note, we are some > ways off from that as yet.* > > 1. Anyone working on the docs? > > *[NS] The tutorials on F* and Low*, the wiki and our papers are what we > have so far as documentation. We expect to write more tutorials, including > one for Meta-F* in the near future. We often discuss consolidating all our > existing documentation (such as it is) into a manual, but no one is working > on that yet.* > > 1. Are there community groups for those and other tasks? > > *[NS] We have an fstar channel on functionalprogramming.slack.com > <http://functionalprogramming.slack.com>: I encourage you to sign up there > and ask questions. FYI, many of us who work heavily on F* are members of a > private slack group. * > > *Slack is nice for some reasons, but it isn’t great especially because it > doesn’t preserve history very well. We are discussing alternatives, but > have not settled on anything yet.* > > *Thanks again,* > > *Nik* > > Quite a lot in retrospective... > > > > All the best, > > Christian Nyumbayire >
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
