Hacker News Reader

Comment by thomastjeffery | Hacker News Reader

Then why are we all so interested?

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

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

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.

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.

Reply on news.ycombinator.com