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

F* – A Proof-Oriented Programming Language

fstar-lang.org

Post reply on HN
Print view View original

51–60 of 104 posts

Re: F* – A Proof-Oriented Programming Language

#51

Post by agentultra »

bluGill wrote: post #43
6gvONxR4sf7o wrote: post #41

I wish one of these languages (where you can prove and confirm that your code follows the formal spec) would aim for production use. I was really interested in Lean 4 when I found out that it aims to be a general purpose language, but then I saw that the language manual still has a section titled "Should I use Lean?" that emphasizes it's just a research project not a product and still expects a bunch more breaking ch…

While I agree with that in principal, in talking to people who have actually written proved programs I get the impression they don't think it is practical to prove programs that are more than medium sized. I'd love to prove my code correct, but I deal with 10s of million lines of code and nobody has a clue how you would approach a problem that large (we use C++, but you can select a different language if you want - t…

I talk to folks who are involved in proof engineering and they disagree here. It is possible to prove large systems when you have good automation. But perhaps it's writing the automation that is hard right now due to a small overlap in skills.

Writing the proofs is one thing but writing the automation that scales those proofs to a larger system and which makes it easy to extend the system without breaking the proofs constantly is key and requires more "engineering" focused people rather than proof-focused ones.

Re: F* – A Proof-Oriented Programming Language

#52

Post by ykonstant »

6gvONxR4sf7o wrote: post #41

I wish one of these languages (where you can prove and confirm that your code follows the formal spec) would aim for production use. I was really interested in Lean 4 when I found out that it aims to be a general purpose language, but then I saw that the language manual still has a section titled "Should I use Lean?" that emphasizes it's just a research project not a product and still expects a bunch more breaking ch…

For small projects without tight performance or reliability requirements, Lean 4 is fine. It is lacking a lot in basic I/O functions, but you just yank them directly from the C standard library via the FFI and use them in your code. Don't expect to be able to prove anything about your code, though; just treat Lean as a pure functional language like Haskell but with dependent types and eager default evaluation.

Re: F* – A Proof-Oriented Programming Language

#53

Post by yodsanklai »

6gvONxR4sf7o wrote: post #41

I wish one of these languages (where you can prove and confirm that your code follows the formal spec) would aim for production use. I was really interested in Lean 4 when I found out that it aims to be a general purpose language, but then I saw that the language manual still has a section titled "Should I use Lean?" that emphasizes it's just a research project not a product and still expects a bunch more breaking ch…

I wonder how that is compatible with the industry requirements, and even with software engineering in general. A lot of the code we write is short lived, either because we're iterating, or because features aren't used anymore. Also, bugs aren't the end of the world most of the time. You don't aim for 100% correctness, but for something that provides value to users and it's better than your competitors. Formal proofs may be useful in some case, but I don't see them outside very niche fields. Even regular static types can be argued against.

Re: F* – A Proof-Oriented Programming Language

#54

Post by chuckadams »

debugnik wrote: post #22
seanw444 wrote: post #15

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

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.

Yeesh, avoiding obvious Russian-isms is one thing, but a common suffix? I say Nyet! Anyone triggered by that isn’t worth accommodating.

Re: F* – A Proof-Oriented Programming Language

#55

Post by chuckadams »

082349872349872 wrote: post #49
User23 wrote: post #39

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

> looking at your code and asking yourself "what has to be true for this to work?" Wait a moment: are there people who write and ship code without continually asking this question, at least to handwaving precision?

They internalize it with tacit assumptions and let runtime exceptions deal with it when the assumptions are violated. We all do this to some extent, and not just in programming, but many people are a lot more YOLO about it when the language allows it (see “duck typing”)

Re: F* – A Proof-Oriented Programming Language

#56

Post by celdon25 »

tombert wrote: post #32
toasted-subs wrote: post #25

Earlier quoted context omitted.

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.

I used F# at realtyshares in 2017. Didn't think it was particularly great for anything except Payment processing. The F# tools were only good with VS IDE on Windows at the time. I would probably use it again though, the REPL is much better than anything C# has to offer.

The Rider release was a shitshow, lots of bugs that went unfixed. Productivity went way down when I had to switch to a mac laptop (keep in mind this is 2017 on a Microsoft language). Had similar experiences with Rubymine in 2022 (poor YARD support, lots of bugs in type inference even with simple things, bug tickets left open for years, thank god for Sorbet-lsp). The tooling is probably better these days but I don't trust Jetbrains for anything, they are a rent-seeking company.

Re: F* – A Proof-Oriented Programming Language

#57

Post by unstruktured »

wk_end wrote: post #44
unstruktured wrote: post #11

F* + 1ml ( https://people.mpi-sws.org/~rossberg/1ml/ ) would be the ultimate experience. I was born too early!

Correct me if I'm wrong (I've only dabbled in F* and only briefly read about 1ML) but wouldn't F*'s full dependent types make 1ML redundant? That is, once you've brought types into the value level, modules themselves become redundant - they're just records, and functors are just functions. The point of 1ML, IIUC, is to accomplish a similar unification without demanding full dependent types and the attendant complexit…

Interesting point. I never inferred a strong connection between dependent types and the unification of records and modules. Maybe a real PL theorist around here can provide insights on that subject.

Re: F* – A Proof-Oriented Programming Language

#58

Post by nextaccountic »

tombert wrote: post #50
ReleaseCandidat wrote: post #45

Earlier quoted context omitted.

> Some day, I'd love to write proofs instead of tests in some places. Believe my, you only want to do that if the proof assistent accepts "I leave the details as an exercise to the reader" ;)

I do a lot of work with Isabelle, and when doing proofs, you can use the word "sorry" to basically say "this is true because I said it's true okay". It's become a running joke in my grad school of "when in doubt, there's always 'proof by sorry'". I'm not as familiar with a lot of the other proof assistants but I suspect there are similar constructs?

> I do a lot of work with Isabelle, and when doing proofs, you can use the word "sorry" to basically say "this is true because I said it's true okay".

I always thought that unsafe { .. } blocks in Rust should be called trustme { .. }

But sorry { .. } is even better!

Re: F* – A Proof-Oriented Programming Language

#59

Post by neonsunset »

celdon25 wrote: post #56
tombert wrote: post #32

Earlier quoted context omitted.

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.

I used F# at realtyshares in 2017. Didn't think it was particularly great for anything except Payment processing. The F# tools were only good with VS IDE on Windows at the time. I would probably use it again though, the REPL is much better than anything C# has to offer. The Rider release was a shitshow, lots of bugs that went unfixed. Productivity went way down when I had to switch to a mac laptop (keep in mind this…

2017 was right as the very first releases of .NET Core 1, 1.1 and 2.0 were happening.

It’s most likely your experience today would be a polar opposite to this.

Post reply on HN