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

61–70 of 104 posts

Re: F* – A Proof-Oriented Programming Language

#61

Post by tombert »

nextaccountic wrote: post #58
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?

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

Yeah, it's pretty funny to see the first draft of anything I'm trying to prove; it'll be polluted with sorry's everywhere; it comes off as the most apologetic, completely un-confident bit of math you can think of.

The worst part is when you forget to remove a sorry (or three) because of a linked file you didn't check, and you submit stuff to other people on the team thinking you discovered something pretty cool, only to find out that you didn't actually prove anything.

Re: F* – A Proof-Oriented Programming Language

#62

Post by eggy »

debugnik wrote: post #17
eggy wrote: post #5

I prefer F#/F* syntax, but I had to go with Ada/SPARK2014 for the safety-related control systems I am trying to verify formally and use for high-integrity applications. Rust is making some inroads with AdaCore and Ferrous Systems partnering on providing formal verification tools for Rust like they do for Ada/SPARK2014, but Rust still doesn't have a published standard like C, Common Lisp, Prolog, Fortran, COBOL, etc.…

> with AdaCore and Ferrous Systems partnering I thought the partnership was already over? AdaCore left Ferrocene, and released its own support for a Rust toolchain lacking formal verification tools.

Very well might be the case. I am speaking on old news. I would guess the lack of an official published standard makes it hard to create tools and support them over time - a moving target.

Re: F* – A Proof-Oriented Programming Language

#63

Post by nequo »

ykonstant wrote: post #52
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.

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?

Re: F* – A Proof-Oriented Programming Language

#64

Post by ykonstant »

nequo wrote: post #63
ykonstant wrote: post #52

Earlier quoted context omitted.

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.

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?

By far the main impediment is that the current community does not care about this use-case. Lean's proof system works mainly by using its metaprogramming aspects to write macro-type objects called tactics; they perform transformations on the goals of your proof to simplify or dispatch them.

[Note that this meta-programming is very powerful, but also extremely hard to use from what I have managed to see; do not expect LISP style ergonomics here. It doesn't help that the meta-programming book shows some trivial examples of macro rules and then delves deep into proof tactics for the next 2 chapters, leaving the reader who wants general code transformations stranded].

In order to use Lean for proving properties for serious amounts of code, you need to write an entire tactics library similar to mathlib (but for code). Nobody has done this. Maybe it is reasonably hard, or maybe unreasonably hard; the point is, there is no serious collaborative effort that I know of.

Re: F* – A Proof-Oriented Programming Language

#65

Post by mkehrt »

samueldurante wrote: post #30
bmitc wrote: post #27

I'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.

I'd assume both are named after System F, the Simply Typed Lambda Calculus enriched with a variety of types of what would widely be called generics.

Re: F* – A Proof-Oriented Programming Language

#66

Post by ReleaseCandidat »

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?

Coq has "admitted" (or "admit"), but sorry is of course way better :). Lean also has "admit".

Re: F* – A Proof-Oriented Programming Language

#67

Post by ReleaseCandidat »

nextaccountic wrote: post #58
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?

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

My favorite is accursedUnutterablePerformIO https://hackage.haskell.org/package/bytestring-0.12.1.0/docs...

    This "function" has a superficial similarity to unsafePerformIO but it is in fact a malevolent agent of chaos. It unpicks the seams of reality (and the IO monad) so that the normal rules no longer apply. It lulls you into thinking it is reasonable, but when you are not looking it stabs you in the back and aliases all of your mutable buffers. The carcass of many a seasoned Haskell programmer lie strewn at its feet.

Re: F* – A Proof-Oriented Programming Language

#68

Post by nequo »

ykonstant wrote: post #64
nequo wrote: post #63

Earlier quoted context omitted.

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?

By far the main impediment is that the current community does not care about this use-case. Lean's proof system works mainly by using its metaprogramming aspects to write macro-type objects called tactics; they perform transformations on the goals of your proof to simplify or dispatch them. [Note that this meta-programming is very powerful, but also extremely hard to use from what I have managed to see; do not expect…

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?

Re: F* – A Proof-Oriented Programming Language

#69

Post by eggy »

ykonstant wrote: post #26
jfoutz wrote: post #4

Earlier quoted context omitted.

Lately I've been dabbling with lean. pretty tight vs code integration. I don't know why I keep getting pulled toward dependent types, like a damn moth to a flame. I get a little scorched, then, oh I should try ... But yeah, compiler checked properties are something kinda magical. Even more when you can specify the property to check.

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.

Re: F* – A Proof-Oriented Programming Language

#70

Post by ykonstant »

nequo wrote: post #68
ykonstant wrote: post #64

Earlier quoted context omitted.

By far the main impediment is that the current community does not care about this use-case. Lean's proof system works mainly by using its metaprogramming aspects to write macro-type objects called tactics; they perform transformations on the goals of your proof to simplify or dispatch them. [Note that this meta-programming is very powerful, but also extremely hard to use from what I have managed to see; do not expect…

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 Haskell. If Lean ever gets the libraries Haskell has, I will be really excited.

Post reply on HN