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

81–90 of 104 posts

Re: F* – A Proof-Oriented Programming Language

#81

Post by dang »

Related. Others?

The F* Programming Language - https://news.ycombinator.com/item?id=31517176 - May 2022 (6 comments)

Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=25629058 - Jan 2021 (76 comments)

F* – An ML-like functional programming language aimed at program verification - https://news.ycombinator.com/item?id=15582969 - Oct 2017 (95 comments)

KreMlin: from (a subset of) F* to C - https://news.ycombinator.com/item?id=12753788 - Oct 2016 (2 comments)

Verified Programming in F*: A Tutorial - https://news.ycombinator.com/item?id=10949288 - Jan 2016 (28 comments)

F*: A Verifying ML Compiler for Distributed Programming - https://news.ycombinator.com/item?id=2663240 - June 2011 (9 comments)

Re: F* – A Proof-Oriented Programming Language

#82

Post by Nevermark »

naasking wrote: post #75
dunham wrote: post #72

Earlier quoted context omitted.

Lean has `sorry` and Idris has `believe_me`. Recalling my math education, I would think the appropriate keyword would be `clearly`.

> Recalling my math education, I would think the appropriate keyword would be `clearly` I prefer the slightly more ominous "surely".

"Obviously" casts a nice aspersion upon anyone so uncouth as to question its validity.

Of course, any junior member of a team that is willing to stand up and state that, no, the assertion is anything but obvious to them, should get an immediate promotion, and be quickly moved to another group!

Re: F* – A Proof-Oriented Programming Language

#83

Post by 082349872349872 »

vinnyvichy wrote: post #80
082349872349872 wrote: post #49

Earlier quoted context omitted.

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

It takes effort for me to compute whether grandfather is de gauche or de droite.. the better question to ask yourself continuously is whether: does this noise (spaghetti/imprecision in this context) improve or remove performance ((0-1) though the 2 questions are related; it's enough to point out that if necessity is the mother of invention, then paradox is the father of discovery)? (0-1) https://quillette.com/2022/04…

thanks for these and the other (sps)! atm I'm busy altering the position of matter at or near the earth's surface relative to other matter, so it may be a week or two before I'm back to the more intellectual exercise of altering the truthiness of symbols in strings or graphs relative to other symbols...

Re: F* – A Proof-Oriented Programming Language

#84

Post by eggy »

ykonstant wrote: post #71
eggy wrote: post #69

Earlier quoted context omitted.

I have heard of Lean, but I just took a look for the first time. Certainly, much more Idris/Haskelly than the OCamlish F*. Are there libraries available for general programming in Lean? Can you compile to another lower-level language like C? I would be interested in writing some embedded code that could formally be verified. Right now, I have put some time in to SPARK2014, the subset of Ada.

Lean in fact compiles to C so the C FFI is trivial to use. However, the only general programming facilities Lean has seem to be those required to bootstrap the language. I find it equal amounts funny and sad that you still cannot get the Unix epoch in Lean; you need to call the C functions through the FFI. For verifying code Lean is not great right now (see a sibling comment in this post). For embedded code in partic…

Thanks, I had looked at ATS many years ago, but I had forgotten about it. I'm going to look at both Lean and ATS, but I guess I'll stick with SPARK2014 for work now.

Re: F* – A Proof-Oriented Programming Language

#85

Post by vinnyvichy »

082349872349872 wrote: post #83
vinnyvichy wrote: post #80

Earlier quoted context omitted.

It takes effort for me to compute whether grandfather is de gauche or de droite.. the better question to ask yourself continuously is whether: does this noise (spaghetti/imprecision in this context) improve or remove performance ((0-1) though the 2 questions are related; it's enough to point out that if necessity is the mother of invention, then paradox is the father of discovery)? (0-1) https://quillette.com/2022/04…

thanks for these and the other (sps)! atm I'm busy altering the position of matter at or near the earth's surface relative to other matter, so it may be a week or two before I'm back to the more intellectual exercise of altering the truthiness of symbols in strings or graphs relative to other symbols...

Ah what shall we do if our beloved HN weren't an obligate asynchrotroph :) Passive consumption recommendation (fit for travel plausibly even) is: to «Das Glasperlenspiel» the postpostmodern (but merely pre-eschatological) riposte could only be «Anathem» --- had to complete the commutative diagram.

(0)https://ironichles.livejournal.com/56695.html

Re: F* – A Proof-Oriented Programming Language

#86

Post by bluGill »

agentultra wrote: post #51
bluGill wrote: post #43

Earlier quoted context omitted.

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…

I've talked to people on both sides of that question. Some think you can (but have had little success in convincing anyone to do it), others think you cannot.

Re: F* – A Proof-Oriented Programming Language

#87

Post by tombert »

williamcotton wrote: post #33
onhacker wrote: post #6

Earlier quoted context omitted.

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.

I haven't really used the Ionide plugin for VSCode, but I did make pretty liberal use of the Emacs plugin (well, Spacemacs), and it was pretty solid. I used it almost exclusively for about a year; I don't know if the Emacs plugin uses Ionide behind the scenes, but I thought it was pretty decent overall.

Still, once Rider got a few updates and was stable, it was kind of hard to go back. I'm a pretty dedicated Vim dude normally, but for a lot of "enterprisey" things like .NET and Java the ability to do smart refactoring of lots of files and integrated debuggers really do become a pretty substantial value-add for me.

Re: F* – A Proof-Oriented Programming Language

#88

Post by Tainnor »

ykonstant wrote: post #70
nequo wrote: post #68

Earlier quoted context omitted.

Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?

Probably, from what people are telling me. But Coq is not a general purpose language, it is a dedicated theorem prover. I don't use Lean as a theorem prover for code (only for mathematics) and I myself don't do any code formalization unless someone offers to pay me. The reason I code in Lean is because I find it fun, and I think it is a very nice general purpose language; for instance, I like Lean much better than Ha…

I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?

Re: F* – A Proof-Oriented Programming Language

#89

Post by 6gvONxR4sf7o »

amw-zero wrote: post #77
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…

Code written in F* is running in Firefox, Linux, Windows, and Azure: https://project-everest.github.io/ .

Cool! Thanks for the link.

Re: F* – A Proof-Oriented Programming Language

#90

Post by mikhailfranco »

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…

It seems a practical system would do all of the above:

- attempt a proof, could pass or fail, but if it times out, then fall back to...

- property-based test case generation, using logical statements and data generators, shrinking, etc.; many will pass, some will fail, but if some time out ...

- generate simple tests, and edge cases, which may trivially pass, but could be edited by hand to become more useful

If you add a timeout, then exponential runtimes, and even the Halting Problem, always give an answer, even if the answer is to try something simpler.

Post reply on HN