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
