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

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.)

Also

> if you've worked with other proof oriented languages.

That's doing a lot of heavy lifting.

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!

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

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.