← Back to context

Comment by thomastjeffery

9 hours ago

Then why are we all so interested?

Examples provide more than syntax. It's the semantics that we care about most.

3 comments

thomastjeffery

Reply
aleph_minus_one  8 hours 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-i...

> https://fstar-lang.org/tutorial/

  • derdi  4 hours 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/ and Lean https://lean-lang.org/ both manage to do this.

    • rybosome  1 hour 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.