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

71–80 of 104 posts

Re: F* – A Proof-Oriented Programming Language

#71

Post by ykonstant »

eggy wrote: post #69
ykonstant wrote: post #26

Earlier quoted context omitted.

Lean is lovely, but those of us using it for general purpose programming are a lonely bunch; virtually all discussion on Zulip is about mathlib and tactics (which is understandable).

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 particular, I remember there was a low-level formalizer, but I cannot remember what it was. This post here has many discussions and links: https://news.ycombinator.com/item?id=31775216

Maybe I am remembering this: https://en.wikipedia.org/wiki/ATS_(programming_language)

But I was under the impression there was an almost assembly-level functional programming language with formal verification capabilities; I cannot recall it.

Re: F* – A Proof-Oriented Programming Language

#72

Post by dunham »

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?

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

Re: F* – A Proof-Oriented Programming Language

#73

Post by rtpg »

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…

Well Coq is used to build a C compiler used in aerospace. At the very least you could write "trricky" stuff in that, and then use the compiled artefacts in your toolkit.

I get the general complaint, though. I wish I could have the syntax-based interactive proof system everywhere.

Re: F* – A Proof-Oriented Programming Language

#75

Post by naasking »

dunham wrote: post #72
tombert wrote: post #50

Earlier quoted context omitted.

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?

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

Re: F* – A Proof-Oriented Programming Language

#76

Post by saurik »

seanw444 wrote: post #46
wk_end wrote: post #38

Earlier quoted context omitted.

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

Stalin never earned the same perception as Hitler, probably because he won and Hitler didn't. History is written by the victors. There's a reason the cliche move in politics is to call your opponent "literally Hitler" and not "literally Stalin". That said, I doubt any tool named "Stalin" would gain any major traction. Adopting such a tool would be a huge liability for a company.

I always figured this would be the correct name for a tool designed to erase unwanted objects out of photos (whether using classic techniques or AI, whatever).

Re: F* – A Proof-Oriented Programming Language

#77

Post by amw-zero »

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

Re: F* – A Proof-Oriented Programming Language

#78

Post by happypumpkin »

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

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

Maybe try looking for Clojure jobs? They aren't super common but are a lot more so than any other lisps or functional languages that I'm aware of (except maybe Scala).

Re: F* – A Proof-Oriented Programming Language

#79

Post by daxfohl »

lambdanik wrote: post #19
daxfohl wrote: post #13

Earlier quoted context omitted.

I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-worl…

F* existed before Project Everest, but Everest did power a lot of its development. We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/ Some of it is deployed in production systems: * Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-h…

So _would_ it possibly be useful for business apps? Or is that still a long way off?

Re: F* – A Proof-Oriented Programming Language

#80

Post by vinnyvichy »

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?

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/05/noise-a-flaw-in-human-judgm...

https://www.newscientist.com/article/2431131-buildings-that-...

Post reply on HN