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: 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
