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

Clicked like 5 pages and never found 1 code example.

Idk why languages don't have their syntax in a sandbox front-and-center on the home page.

It's like a video game site with zero screenshots or videos (also rampant).

New programming languages I want 2 things:

1. What does the syntax look like

2. Why would I use this language

Talk about the proof logic, show the syntax, thank you

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

I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.

I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages.

Is this used in the industry ? And for what kind of software ?

I guess responsive stylesheets can't be implemented without side effects...

Would this language be useful for implementing compilers and formally proving things about them?

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?

[dead]

[dead]

[flagged]

[flagged]