It makes me miss my time spent tinkering with Idris :)
F* – A Proof-Oriented Programming Language
31–40 of 104 posts
Re: F* – A Proof-Oriented Programming Language
#32Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my te…
Where do you even find orgs that let you program in those fun langs? University jobs?
I was working for Jet.com, it was one of the very few places that did F#. The reason I was hired was because I had Haskell experience from working at NYU as an engineer before.
Re: F* – A Proof-Oriented Programming Language
#33Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my te…
After C#, I learned F#, I loved language structure, but I was not able to run it on production effectively. A language isn't enough, a language recognized from its support in ide/production and community
Ionide, The F# language server, is excellent.
I use F# in .NET Interactive Jupyter notebooks daily at work and it works quite well.
The community around the language is very helpful and the Discord is great for all sorts of issues ranging from beginner to advanced.
I love the Fable compiler which targets JS, TS, Python and Rust and makes for a wonderful way to share a domain design across multiple code bases.
Re: F* – A Proof-Oriented Programming Language
#34I've never understood the relationship between F# and F*. I had previously come to the conclusion that F* was merely inspired by F#'s syntax and base-level semantics but that was where the relationship ends. As far as I can tell, F* is not a .NET language and doesn't run on the CLR. Is that correct? In the description it says it compiles to OCaml, which confuses me even more about the F* naming. What is the relations…
I believe that F* is named purely for marketing purposes, or perhaps to specify another programming language with syntax derived from OCaml. But other than that, I don't think it has any other relation.
Not just marketing ...
About the name: https://fstar-lang.org/tutorial/book/intro.html#a-bit-of-f-h...
Re: F* – A Proof-Oriented Programming Language
#35Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my te…
Where do you even find orgs that let you program in those fun langs? University jobs?
[dead]
Re: F* – A Proof-Oriented Programming Language
#36Earlier quoted context omitted.
I'm guessing they came up with the wordplay before the invasion, and then regretted it because the reference suddenly stopped being purely historical. And I get it, I've been phasing out this username, which I picked with bad timing, to avoid unintended connotations, even though I was simply thinking of Robotnik and not anything russian. I've got nothing to do with their language, so it just isn't worth it.
-nik is a suffix which exists in all Slavic languages, including Ukrainian. Nothing specifically Russian about it.
And even if it was, poking gentle fun at a Russian suffix would not be an endorsement of the invasion.
Re: F* – A Proof-Oriented Programming Language
#37Earlier quoted context omitted.
I'm guessing they came up with the wordplay before the invasion, and then regretted it because the reference suddenly stopped being purely historical. And I get it, I've been phasing out this username, which I picked with bad timing, to avoid unintended connotations, even though I was simply thinking of Robotnik and not anything russian. I've got nothing to do with their language, so it just isn't worth it.
-nik is a suffix which exists in all Slavic languages, including Ukrainian. Nothing specifically Russian about it.
I, personally, am aware, but I'm not so sure everyone who will read my username knows that, and there's enough war-related shilling around (and suspicion thereof) that the pun simply isn't worth it.
Re: F* – A Proof-Oriented Programming Language
#38Earlier quoted context omitted.
I'm curious why the resemblance and homage to the Soviet Union in the first place, but I find it sad that people feel the need to rebrand things like this, to avoid the mob. Just because I don't like communism, doesn't mean people can't have things named after one of recent history's most well-known superpowers, with admittedly cool style.
Agree, and there are other projects with fun names like https://en.wikipedia.org/wiki/Stalin_(Scheme_implementation)
It's odd how this is deemed acceptable - Wikipedia explains that the joke is in reference to its "brutal" optimization, which I'm sure eastern Europeans find hilarious (they might, they're known for their grim sense of humour) - but no one would seriously consider naming, say, their fork of the GNU assembler "Hitler".
Re: F* – A Proof-Oriented Programming Language
#39They wrapped Dijkstra and Scholten's predicate transformer semantics [2] in a monad[1]! This almost irrationally pleases me. I'd really love the general concept to get wider traction too. While it's particularly useful for this kind of deep language design, a weakest precondition calculus be used manually when writing code[3] without any particular additional effort once proficiency has been achieved. To use an analogy, it's like the old trick of solving a maze by starting at the end and working backward. Often it ends up being considerably easier.
[1] https://link.springer.com/book/10.1007/978-1-4612-3228-5
[2] https://dl.acm.org/doi/10.1145/2499370.2491978
[3] It pretty much boils down to looking at your code and asking yourself "what has to be true for this to work?" and then writing code that ensures whatever is necessary is true for all possible code paths. Naturally that means limiting possible code paths. There's just one more reason why spaghetti code is bad.
Re: F* – A Proof-Oriented Programming Language
#40Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my te…
Where do you even find orgs that let you program in those fun langs? University jobs?
There are some trading companies as well, I guess because it's ocaml adjacent.