Thank you Jonathan! I will inspect! So far my first preoccupation is to get a flexible enough Makefile, so I'm still stack on previous points. I've seen that FStar.Util has most of what could be used in IO outside printing and basic file management, so I guess there is not that much to extend (although, as a noob, I should say that I got some problems on finding those functions in the sources).
Low* IO so far is quite not an easy bite for me right now as, as you said, it requires more upfront conceptual work. Gonna tell you in the next days I guess. All the bests! Christian Il giorno mar 15 gen 2019 alle ore 13:03 Jonathan Protzenko < pr...@microsoft.com> ha scritto: > Hello Christian, > > Responding more specifically to your KreMLin/Low* questions... > > Most of the systems-level modeling in Low* is fairly primitive, as > whatever little there is was only designed to support the creation of > minimal tests or proof-of-concepts. As such, stdin was simply never added. > Low* definitely needs proper systems libraries, but this is a big task, as > it requires solving several library issues together: IO, but also a proper > model of mutable and constant strings, etc. > > That being said, you can roll out your own systems libraries in your own > project without having to extend kremlib. Looking at tests/server or > tests/hello-system in the kremlin repository, you should find some basics > to help you get started with creating a "mini systems lib" for your > project, with an F* interface and/or model, along with a C implementation. > I'm happy to help on Slack with this. > > Once you get something working, I would hope that we can go through a pull > request, adding F* modules to ulib in the LowStar namespace. This would > also be a good way to review and discuss together to make sure we come up > with something compelling once it lands in ulib. > > Hope this helps! > > ~ jonathan > ------------------------------ > *From:* fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf > of Christian Nyumbayire via fstar-club <fstar-club@lists.gforge.inria.fr> > *Sent:* Wednesday, January 9, 2019 6:41 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. > 2. Is there any reason there is no stdin in kremlib, even as a channel? > 3. What is the proper way to extend kremlib? (I've seen the include) > 4. 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. > 5. Anyone working on the docs? > 6. Are there community groups for those and other tasks? > > 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
