Live data from Hacker News

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

fstar-lang.org

91–100 of 107 posts

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

#91
post #62

Earlier quoted context omitted.

> have to fix it up manually Any editor written or actively maintained in the current century does this automatically for you. (Yes that obviously includes Emacs and Vim).

But that doesn't work if the indentation carries semantic meaning; you can't change the indentation without changing the meaning. Maybe you can correct syntactically-incorrect spacing (e.g. change 3 spaces to 4 spaces), but not much beyond that.

The Vim I use increases the indent of a code block when I ask it to. Just like it places a closing curly brace at the point where I tell it to. I don't see the fundamental difference between these two things.

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

#92

Earlier quoted context omitted.

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)

> have to fix it up manually Any editor written or actively maintained in the current century does this automatically for you. (Yes that obviously includes Emacs and Vim).

In gdb? It's a shame gdb picked python

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

#93

- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust

Your question is why don't we have a language that performs much better than the best-performing languages? Why would you expect such a thing?

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

#94

- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust

There's nim [1] which is aiming for the same thing - syntax similar to python and performance similar to C++, zig etc.

1 - https://nim-lang.org/

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

#95
post #90

- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust

That language is basically F#, except for perhaps the performance claims. But F# is definitely not a slow language.

Matthew Crews has a done a number of videos on high-performance F# and there are some things you can do that give a big boost over the default coding approach.

Why F# for Performance -- https://www.youtube.com/watch?v=EIBRoNEpg6c

F# for Performance-Critical Code -- https://www.youtube.com/watch?v=NZ5Lwzrdoe8

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

#96

- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust

Your question is why don't we have a language that performs much better than the best-performing languages? Why would you expect such a thing?

- another stupid question: what exactly makes the best performing languages perform so

- 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?

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

#97
post #62

Earlier quoted context omitted.

But that doesn't work if the indentation carries semantic meaning; you can't change the indentation without changing the meaning. Maybe you can correct syntactically-incorrect spacing (e.g. change 3 spaces to 4 spaces), but not much beyond that.

The Vim I use increases the indent of a code block when I ask it to. Just like it places a closing curly brace at the point where I tell it to. I don't see the fundamental difference between these two things.

But you have to ask it to, and by the right amount for every line/sub-block. If you accidentally get one line wrong, it could be a silent bug. In a language without significant indentation, as long as braces are preserved, once you are done moving code around a single autoformat will fix everything including nested blocks. And if you forget a brace, it's an error instead of a silent bug

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

#98

Earlier quoted context omitted.

Your question is why don't we have a language that performs much better than the best-performing languages? Why would you expect such a thing?

- another stupid question: what exactly makes the best performing languages perform so - 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?

> what exactly makes the best performing languages perform so

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.

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

#99
post #80

Earlier quoted context omitted.

You mean add indentation to code where it shouldn't matter?

We need auto-unformatting too? Auto formatting that doesn't get added as a git change?

I just find it funny that the auto formatting adds the spacing to a very specific style, but requiring spacing is too much for some, readability is much richer in most Python projects I've opened (I can't think of one where it was terrible) compared to Java and C# projects I've opened due to people in Python following coding style standards more frequently, PEP-8 is king.

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

#100
post #12

Earlier quoted context omitted.

I'm the opposite: when landing in a programming language site I want to know the user case the authors had in mind, the memory model, the type system, the compilation targets, the data layout, the control structures, and only at the end just check that the syntax is not indentation based.

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

indentation based immediately implies no safe copy pasting, and you can't count on a formatter to untangle the havoc pasting some code can wreak
Post reply on HN