3 ms·

That’s because syntax is the least interesting part of F*.

• thomastjeffery 3mo ago
  Then why are we all so interested? Examples provide more than syntax. It's the semantics that we care about most.
  • aleph_minus_one 3mo ago
    > Examples provide more than syntax. It's the semantics that we care about most. ... and this semantics is explained in a quite encompassing way in the introductory notes "Proof-Oriented Programming in F*": > https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf https://fstar-lang.org/tutorial/proof-oriented-programming-i... > https://fstar-lang.org/tutorial/ https://fstar-lang.org/tutorial/
    • derdi 3mo ago
      The OP doesn't want encompassing, they want the following example from the tutorial on the front page: type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1) let rec append #a #n #m (v1:vec a n) (v2:vec a m) : vec a (n + m) = match v1 with | Nil -> v2 | Cons hd tl -> Cons hd (append tl v2) This is a completely reasonable thing to want and expect. Edit: For comparison, Rocq https://rocq-prover.org/ https://rocq-prover.org/ and Lean https://lean-lang.org/ https://lean-lang.org/ both manage to do this.
      • rybosome 3mo ago
        I'm not the OP, but this is exactly my interpretation, and my gripe with the homepage as well in lacking this concise yet powerful example. You can tell a lot about a programming language by looking at the right snippet.