Re: [fstar-club] Noob questions

[Christian Nyumbayire via fstar-club]

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  on behalf
> of Christian Nyumbayire via fstar-club 
> *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

Re: [fstar-club] Noob questions

[Jonathan Protzenko via fstar-club]

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  on behalf of 
Christian Nyumbayire via fstar-club 
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

Re: [fstar-club] Noob questions

[Christian Nyumbayire via fstar-club]

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

Re: [fstar-club] Noob questions

[Nikhil Swamy via fstar-club]

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