F*: A general-purpose proof-oriented programming language
fstar-lang.org
fstar-lang.org
Does it get basic stuff like subtraction and u8 right, unlike Lean?
This is demonstrably untrue.
In any case that post is pretty unpersuasive. Basically saying it's too tedious to do it right, in a language whose whole purpose is tediously doing things right!
Probably the better conclusion is that more proof automation is needed for simple things like "this number is not negative" so it is less tedious.
(I'm not a Lean expert but I was totally put off by it happily accept a uint8 with value 300.)
Is this used in the industry ? And for what kind of software ?
https://www.microsoft.com/en-us/research/blog/everparse-hard...
Some Windows things too I think (I think F* is partially funded by Microsoft Research)
They actually wrote a whole verified TLS implementation in F* and discovered a bunch of TLS vulnerabilities in other implementations
https://project-everest.github.io/
https://github.com/hacl-star/hacl-star
https://blog.mozilla.org/security/2017/09/13/verified-crypto... (note, that's from 2017, so, not exactly new.. not sure how this is not more well known)
Why F# for Performance -- https://www.youtube.com/watch?v=EIBRoNEpg6c
F# for Performance-Critical Code -- https://www.youtube.com/watch?v=NZ5Lwzrdoe8
- c gets compiled to obj files and these are run natively by each cpu are they not?
- isnt there a way to say translate a high level language directly into higly optimized machine code very specific to each processor model in the world? arent there like only a 100 processor models at max?
There's a multitude of factors. Broadly speaking, to achieve high performance on modern hardware you want one or more of:
- Control over emitted code and/or data structures. You tend to see this most prominently with "low-level" programming languages like C or C++, especially when coupled with extensions like SIMD intrinsics or inline assembly.
- Semantics/features that make life easier for the optimizer/runtime. Types are an obvious example here, but other things like annotations (e.g., `restrict` in C, `std::unreachable` or `[[likely]]`/`[[unlikely]]` in C++) and the right abstractions (e.g., C++ expression templates) can all make it easier to get good performance.
- Less dynamic semantics. Stuff that changes or needs to be resolved at runtime tends to make optimizers/hardware unhappy, so if you want performance you either want to avoid writing such constructs in the first place (e.g., writing code that doesn't involve pointer chasing) or spend engineering effort to reduce/eliminate their impact at runtime (e.g., the JVM, though for best effect you tend to need to write your code in a specific style anyways).
There's probably other factors I'm forgetting...
> c gets compiled to obj files and these are run natively by each cpu are they not?
To a first approximation, sure.
> isnt there a way to say translate a high level language directly into higly optimized machine code very specific to each processor model in the world?
This is basically one of the things JITs promise - the ability to optimize a program specifically for the computer it is running on.
It's technically possible to offer processor-specific binaries with ahead-of-time compilation as well (e.g., passing the appropriate -march flag to GCC/Clang/etc.), but I think for most programs you'll usually see different binaries for different CPU families based on the instruction set(s) they implement (e.g., one binary for x86-64v2, one for x86-64v3, one for x86-64v4, etc.) rather than processor-specific binaries.
Its type system is the proof language/metatheory for making propositions, and its programs are their proofs, and there’s an intermediate form, core F*, that we elaborate to, a partial evaluation phase where we actually use the dependent types to simplify our AST, then codegen/lowering. In your analogy, I would call their core IR the bridge I guess? To clarify, I’m not trying to be a dick, I’m trying to sus out if I’ve understood you correctly
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
FYI: The link to this tutorial is unluckily a little bit obscured on the F* website: Go to
> https://fstar-lang.org/index.html#learn (1)
and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".
In the section of (1) also the PDF version is linked:
> https://fstar-lang.org/tutorial/proof-oriented-programming-i...
But I do see the editor to try it.
I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.
It matters a lot how the syntax looks IMO and seeing how, say, an API is scaffolded, helps understand a lot about the language in one glance
Edit: Page 18 of the PDF. That's the first time I found what the code looks like, thanks for sharing!
Often the reason is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.
--
If you want a programming language that "just" enables you to write something well-understood (in particular in the area of web development) like your suggested
> "HTTP server", "hello world", "todo list app"
in a perhaps just a little bit more elegant/concise way, just look at which web development language/framework is currently fashionable on HN.
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
> 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 for what kind of problems people are using F*.
Spoiler alert: these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].
This is exactly the reason why I wrote further above:
> Often the reason [why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app"] is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.
Ok, what kinds of problems are they?
And ideally - what does a simple solution look like in F-star?
Set me on the path to installing the thing (ideally above the fold)
> And ideally - what does a simple solution look like in F-star?
RTFM
Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.
> Set me on the path to installing the thing (ideally above the fold)
How to install this thing:
1. Read https://fstar-lang.org/index.html#download
2. Go to the GitHub page linked there: https://github.com/fstarlang/fstar/releases
3. Download F* for an operating system of your choice there.
Reading the exchange it seems like you got caught up on the illustrative examples the other person used. If a web server isn't a good example of a simple problem for F* the landing page should have an example of something that is. It shouldn't take going through that many steps to understand the so what.
* Error 17 at Welcome.fst(24,0-28,30):
- Could not start SMT solver process.
- Command: ‘/home/site/wwwroot/fstar/bin/z3’
- Exception:
Unix.Unix_error(Unix.ENOENT, "create_process", "/home/site/wwwroot/fstar/bin/z3")
1 error was reported (see above)Also
> if you've worked with other proof oriented languages.
That's doing a lot of heavy lifting.
I don't find F* syntax anymore intimidating than Haskell, Scala, Mercury, Prolog, etc. aka the hard languages. I love Ruby and I didn't find it intuitive when I first began learning it (specifically, the block/lambda passing mechanism).
I'm old enough that I've had the pleasure of handholding software engineers through their first anonymous function usage. Effect system, refinement types, totality checker? The best I get is blank stares before they go back to C# and JavaScript. These days I'm just glad they tolerate linq expressions and typescript.
It matters where you're standing for what feels incomprehensible. But then again, you can say the same thing about dwarf fortress.
If it walks like a duck, farts like a dog, and flies like a fish - it's Java$cript.
TypeScript is used by the pious - they think it will bring them closer to God.
> dwarf fortresses that prove code with math
And then there's you guys.
Gattir allar,
aþr gangi fram,
vm scoðaz scyli,
vm scygnaz scyli;
þviat ouist er at vita,
hvar ovinir sitia
a fleti fyr
Who never to himself hath said,
This is my own, my native land!
Whose heart hath ne’er within him burn’d,
As home his footsteps he hath turn’d,
From wandering on a foreign strand!
If such there breathe, go, mark him well;
For him no Minstrel raptures swell;
High though his titles, proud his name,
Boundless his wealth as wish can claim;
Despite those titles, power, and pelf,
The wretch, concentred all in self,
Living, shall forfeit fair renown,
And, doubly dying, shall go down
To the vile dust, from whence he sprung,
Unwept, unhonour’d, and unsung.
Perhaps English is not a native language for zlsa?
I think rixed means "code editing" (I guess that rixed is simply not a native (L1) or excellent L2 English speaker).
And I love that people love indentation based languages so I show them a file with some spurious tabs to see how they feel about indentation causing silent errors.
That said, it is hard-mode:
- You'll have to figure out how to parse it.
- If you want editor support, it's a pain to get tree-sitter to handle it.
- You may not be able to pull off editor operations like "rename" without implementing a pretty printer (a rename might affect indentation).
I think it is helpful for crude error recovery. On parse error, my language will simply skip to the next column 0 token and parse another declaration.
I did not do this (hindsight), but I would recommend arranging the grammar so you only get indented blocks in cases where the previous line ends in a keyword that introduces it. I think python has a trailing `:` every time indentation is introduced, and Elm does this too - in statements like `let` you need a newline after the `let` to get the multi-declaration version. (This addresses the rename issue.)
I think I need to see an example.
foo x y = do a <- something
pure somethingElse
Similarly:
foo x y = let a = something
b = anotherThing
in somethingElse
Edit: This was brought to my attention by an Idris style guide that said: "Indent so that alpha conversion always works with a simple search and replace. In general this would mean starting a new line when starting a new level of indentation."
I find it easy to see if things are on the same indentation. I find it much harder to visually scan for opening and closing braces unless syntax highliting makes them scream at me or they are accompanied by ...indentation.
Any editor written or actively maintained in the current century does this automatically for you. (Yes that obviously includes Emacs and Vim).
Underappreciated benefit of side benefit of indentation based languages: no copy-pasta.
But I clicked one (1) link to the online book and found a thousand?
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...
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)
Edit: For comparison, Rocq https://rocq-prover.org/ and Lean https://lean-lang.org/ both manage to do this.