Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

fstar-lang.org

Post reply on HN
Print view View original

101–107 of 107 posts

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

#101

Post by vrighter »

teiferer wrote: post #57
Georgelemental wrote: post #54

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

no, they can't in indentation based languages. changing indentation implies changing the code. A formatter isn't allowed to do that

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

#102

Post by pvsnp »

aw1621107 wrote: post #68
rixed wrote: post #28

Earlier quoted context omitted.

What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?

I think it's meant to be parsed as "I liked being able to (express (calling external libraries))", not "I liked being able to (express calling) (external libraries)"

Yes. Probably could’ve written it better but I’ve not poked around F* in a while and I was writing on my phone. Say you’re calling an external function implementation in hardware, being able to express those interfaces as external makes it viable to use F* vs assuming everything is open source and introspectable.

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

#103

Post by oxavier »

aw1621107 wrote: post #98
vivzkestrel wrote: post #96

Earlier quoted context omitted.

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

Really appreciate the effort put into a seemingly naive questions, thanks.

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

#104

Post by dunham »

floxy wrote: post #81
dunham wrote: post #38

Earlier quoted context omitted.

I don't mind indentation based languages. I used to hate them, but they've grown on me after using python, Haskell, Idris, Agda, etc. And I ended up making my own language indentation based (it is similar to Idris). 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…

>a rename might affect indentation I think I need to see an example.

It happens when the indentation is established on the same line as other code, so having a rule that you need a newline to start indentation will avoid the issue. Examples from haskell:

    foo x y = do a
Renaming `x` to `xxx` would push the indented block in and the subsequent lines would have to be indented too.

Similarly:

    foo x y = let a = something
                  b = anotherThing
              in somethingElse
Elm avoids this by requiring an newline after the `do` and `let` (if the `let` has multiple assignments).

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

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

#105

Post by floxy »

dunham wrote: post #104
floxy wrote: post #81

Earlier quoted context omitted.

>a rename might affect indentation I think I need to see an example.

It happens when the indentation is established on the same line as other code, so having a rule that you need a newline to start indentation will avoid the issue. Examples from haskell: foo x y = do a Renaming `x` to `xxx` would push the indented block in and the subsequent lines would have to be indented too. Similarly: foo x y = let a = something b = anotherThing in somethingElse Elm avoids this by requiring an new…

Thanks

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

#106

Post by aw1621107 »

oxavier wrote: post #103
aw1621107 wrote: post #98

Earlier quoted context omitted.

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

Really appreciate the effort put into a seemingly naive questions, thanks.

You never know if the person on the other end is going to be one of today's lucky 10000 :P

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

#107

Post by mxkopy »

vivzkestrel wrote: post #87

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

Julia is basically this, i.e. compiled typed python. The nesting for type declarations gets gnarly though, which answers your general question - the really nice language ergonomics cost compute at runtime because that’s the only way you avoid laying everything out beforehand.
Post reply on HN