61–70 of 107 posts
Would this language be useful for implementing compilers and formally proving things about them?
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).
Earlier quoted context omitted.
This is needless fearmongering. F* looks a lot like F# code with semantics you should be familiar with if you've worked with other proof oriented languages. The website design is dated is all. The book gives exactly what the OP wants in the introductory chapter.
Fearmonger? Me? Well I never. 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).
Earlier quoted context omitted.
> 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. 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…
> these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...]. 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.
Earlier quoted context omitted.
Fearmonger? Me? Well I never. Also > if you've worked with other proof oriented languages. That's doing a lot of heavy lifting.
Fearmonger is a little heavy handed but the comparison to Dwarf Fortress is probably too strong. 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.
Earlier quoted context omitted.
Fearmonger is a little heavy handed but the comparison to Dwarf Fortress is probably too strong. 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).
Meanwhile I'm sure there's people out there baffled that anyone finds dwarf fortress challenging to get into. 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 type…
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
I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?
I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages. Is this used in the industry ? And for what kind of software ?
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)
Earlier quoted context omitted.
> 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... > https://fstar-lang.org/tutorial/
The OP doesn't want encompassing, they want the following example from the tutorial on the front page: 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) This is a completely reasonable thing to want and expect. Edit: For comparison,…