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

41–50 of 104 posts

Re: F* – A Proof-Oriented Programming Language

#41

Post by 6gvONxR4sf7o »

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 changes, and so on.

Some day, I'd love to write proofs instead of tests in some places.

Re: F* – A Proof-Oriented Programming Language

#42

Post by wisemang »

seanw444 wrote: post #15
pelagicAustral wrote: post #7

The first thing that came to mind when I entered the site was the resemblance of the classic Soviet iconography to their logo, sans the hammer and sickle, then I checked the repo, and coincidentally, they have a recent commit (`c6fac4d`) titled " kremlin -> karamel " [0] ( [...] a tool for extracting low-level F programs to readable C code*)... Apparently, the commit is one big rename operation from Kremlin to Karame…

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.

Well tbf Kremlin (as typically used) isn’t just a USSR reference it’s a specific place in Moscow. Still used as a metonym for Russia’s government.

That said I do actually love that Soviet propaganda aesthetic. Can appreciate not wanting to be associated with the existing madman running Russia though.

Re: F* – A Proof-Oriented Programming Language

#43

Post by bluGill »

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 - the problem is the size and you can't get around that with a different language

Re: F* – A Proof-Oriented Programming Language

#44

Post by wk_end »

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 complexities they bring.

Re: F* – A Proof-Oriented Programming Language

#45

Post by ReleaseCandidat »

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…

> 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" ;)

Re: F* – A Proof-Oriented Programming Language

#46

Post by seanw444 »

wk_end wrote: post #38
mapcars wrote: post #21

Earlier quoted context omitted.

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

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.

Re: F* – A Proof-Oriented Programming Language

#47

Post by PhunkyPhil »

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…

Surely it wouldn't be aimed at proving a 10 million line black box of code, right?

In my mind it would have to be built from the ground up, sub unit tests for function proofs and maintain 100% coverage as you go along. As long as the constituent parts are proven you don't have to zoom out to a macro level.

Re: F* – A Proof-Oriented Programming Language

#48

Post by Someone »

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…

Divide and conquer does work a bit, though. Languages that support strong encapsulation of various structures will be easier to work with than those that pass pointers around.

As an example, having proofs of various properties of strcat, strcpy, etc. will help less in large programs than having proofs for all Java’s methods on String. In the former, you’ll also have to proof that covers all accesses to your data. In the latter, the JVM guarantees that.

Re: F* – A Proof-Oriented Programming Language

#49

Post by 082349872349872 »

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?

Re: F* – A Proof-Oriented Programming Language

#50

Post by tombert »

ReleaseCandidat wrote: post #45
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…

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

Post reply on HN