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

119 points - today at 12:31 PM

Source

Comments

cyanregiment today at 2:28 PM
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

LelouBil today at 8:18 PM
LelouBil today at 8:06 PM
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 ?

pvsnp today at 2:00 PM
I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
boutell today at 7:05 PM
I guess responsive stylesheets can't be implemented without side effects...
3lambda today at 3:28 PM
Would this language be useful for implementing compilers and formally proving things about them?
IshKebab today at 3:49 PM
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?

rustfreeforme today at 3:34 PM
[dead]
rustfreeforme today at 3:35 PM
[dead]
yourewrongsorry today at 5:08 PM
[flagged]
kirlfiend_grill today at 3:00 PM
[flagged]