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.
F*: A general-purpose proof-oriented programming language
91–100 of 107 posts
Re: F*: A general-purpose proof-oriented programming language
#92Earlier 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).
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
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
Re: F*: A general-purpose proof-oriented programming language
#95- 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.
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?
- 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
#97Earlier 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.
Re: F*: A general-purpose proof-oriented programming language
#98Earlier 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?
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
#99Earlier 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?
Re: F*: A general-purpose proof-oriented programming language
#100Earlier 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?