F*: A proof oriented general purpose programming language
1–10 of 64 posts
Re: F*: A proof oriented general purpose programming language
#2In what situations would one prefer this vs Lean?
This seems to compile to native code if desired, so does that mean it’s faster than Lean?
Forgive me if these are obvious questions, I’m just curious and on my phone right now away from my machine.
Re: F*: A proof oriented general purpose programming language
#3I wonder if the proliferation of programming languages we saw in the last decade is due to the fact that nowadays it's extremely easy to create one or that existing ones sucks?
Re: F*: A proof oriented general purpose programming language
#4In what situations would one prefer this vs Lean? This seems to compile to native code if desired, so does that mean it’s faster than Lean? Forgive me if these are obvious questions, I’m just curious and on my phone right now away from my machine.
Looking at publications on the home pages for both projects it seems F* results in more practical stuff like hardened cryptography and memory allocation libraries, while Lean presents itself as more of an experiment in developing proof assistants.
Re: F*: A proof oriented general purpose programming language
#5I wonder if it's a good idea to pick a name that's hard to search for...
Re: F*: A proof oriented general purpose programming language
#6I wonder if the proliferation of programming languages we saw in the last decade is due to the fact that nowadays it's extremely easy to create one or that existing ones sucks?
F* is older than a decade. Also it's a research project, so quite different than the random "memory safe" language iteration of the day.
Re: F*: A proof oriented general purpose programming language
#7I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the focus on being able to write real programs in it. Most theorem proving languages are focused on mathematics or proving things about a program, and they are very abstract. This language appears to have a goal of bridging the gap and making it simple to write programs and prove parts of them. I believe this is the future of formal languages. If you write something in Rust, it would be great to prove aspects about it. Why not? Well F* is a vision if this future. As proof automation gets better, we will be able to prove many things about our programs, something which is not typically attempted due to difficulty. For instance, imagine proving that a certain path has no allocations, spawns no threads, cannot deadlock, preserves privacy, only modifies a certain subset of global data, is a specific algorithmic complexity, is not subject to timing attacks, maintains the conference of a cache, is memory safe (without a borrow checker). The limit is your imagination and Rice's theorem.
Re: F*: A proof oriented general purpose programming language
#8I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the focus on being able to write real programs in it. Most theorem proving languages are focused on mathematics or proving things about a program, and they are very abstract. This language appears to have a goal of bridging the gap and making it simple to write pr…
https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe
Re: F*: A proof oriented general purpose programming language
#9In what situations would one prefer this vs Lean? This seems to compile to native code if desired, so does that mean it’s faster than Lean? Forgive me if these are obvious questions, I’m just curious and on my phone right now away from my machine.
One technical difference is that F* heavily uses SMT automation, which is less emphasized in Lean (their book even says that F* typechecking is undecidable). F* programmers frequently talk about the language's emphasis on monadic programming, which I'll admit that I don't understand (but would like to!)
Re: F*: A proof oriented general purpose programming language
#10I wonder if the proliferation of programming languages we saw in the last decade is due to the fact that nowadays it's extremely easy to create one or that existing ones sucks?
I think it's because (a) it's become a lot easier to create languages and (b) we're stuck.
I am hoping (a) is straightforward. For (b), I think most of us sense at least intuitively, with different strengths, that our current crop of programming languages are not really good enough. Too low-level, too difficult to get to a more compact and meaningful representation.
LLMs have kinda demonstrated the source for this feeling of unease, by generating quite a bit of code from fairly short natural language instructions. The information density of that generated code can't really be all that high, can it now?
So we have this issue with expressiveness, but we lack the insight required to make substantial progress. So we bounce around along the well-trodden paths of language design, hoping for progress that refuses to materialize.