F*: A general-purpose proof-oriented programming language

Post by cyanregiment » Sun, Aug 02, 2026, 8:11 PM UTC

aleph_minus_one wrote: post #48

cyanregiment wrote: post #45

Earlier quoted context omitted.

> just look at which web framework See, by listing those, you can tell what it is. I imagine the quick project showcase would be different for Swift or for Rust. Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it. Like what kinds of things i can even think of writing with it - an implementation example

> I imagine the quick project showcase would be different for Swift or for Rust. > Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it. I suggest simply having a look at the table of contents of > https://fstar-lang.org/tutorial/proof-oriented-programming-i... This in my opinion gives you a first rough idea…

Post by LelouBil » Sun, Aug 02, 2026, 8:18 PM UTC

Post by derdi » Sun, Aug 02, 2026, 8:46 PM UTC

aleph_minus_one wrote: post #29

thomastjeffery wrote: post #24

Earlier quoted context omitted.

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/

    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)

Post by teiferer » Sun, Aug 02, 2026, 9:16 PM UTC

Georgelemental wrote: post #54

sroerick wrote: post #16

Earlier quoted context omitted.

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

Indentation based is a pain when copy-pasting between contexts with different indentation levels, as you have to fix it up manually, which is error-prone. In languages without it, you can just auto-format. (And even in an editor that doesn't support that, having a second indicator makes it less error-prone to fix manually)

Post by IshKebab » Sun, Aug 02, 2026, 9:26 PM UTC

gugagore wrote: post #56

IshKebab wrote: post #20

F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out. Does it get basic stuff like subtraction and u8 right, unlike Lean?

https://xenaproject.wordpress.com/2020/07/05/division-by-zer...