Re: [fstar-club] KreMLin question about allocation on the heap

Hi Zhiting, We haven't spent a lot of time and effort modeling heap-based allocation, although I believe there's no theoretical reason why we can't do it. It's just that we've been using stack-based allocation for most of our code, so far... perhaps we could have one of our interns over the

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

Correct. There is really no string library except for the few helpers that you have found. Creating a set of helpers that implement the most needed functions would be of course extremely useful. The char type is difficult to deal with, because it is the only C type that is neither signed or

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

Yes, this is something that has poor usability. Prims.string and FStar.String.concat are supported as transition mechanisms to help porting F* programs to Low* but I agree that it's confusing for beginners to have them work "by default".

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin > > I'd expect the following to work, though. Does it? > > let main () = >C.print_string (C.string_of_literal (normalize_term (String.concat ", > " ["hello"; "world"]))); >C.e

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

rly enough. Clément. On 2018-05-02 11:08, Jonathan Protzenko via fstar-club wrote: > Yes, this is something that has poor usability. Prims.string and > FStar.String.concat are supported as transition mechanisms to help porting F* > programs to Low* but I agree that it's confusing for beginners

Re: [fstar-club] Noob questions

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.

Re: [fstar-club] FStar school

Another one is coming up at Daghstul in August, specifically about meta-programming in F*: https://www.cl.cam.ac.uk/events/metaprog/2019/ Hoping to see you at one of those events, ~ jonathan From: fstar-club on behalf of Nikhil Swamy via fstar-club Sent:

Re: [fstar-club] bug report (wrong cast from I32)

Hello Paul and Félix, Thanks for the bug report -- I've filed https://github.com/FStarLang/FStar/issues/1803 Out of curiosity, what was your initial interest in F*? Are you interested in proving some numerical routines? Cheers, ~ jonathan From: fstar-club

[fstar-club] Second and Final Call for Presentations: PriSC 2022 @ POPL 2022

All details are on the PriSC site . Call for Presentations: PriSC 2022 @ POPL 2022 The emerging field of secure compilation aims to preserve security