3 ms·

I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the

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

akkad33 2y ago
https://dafny.org/ 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
- nextos 2y ago
  Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts). It's a great place to start with verification, as proofs are discharged to SAT/SMT, so things are automated. It can get a bit frustrating when automation is not able to prove things, that's the major disadvantage of SAT/SMT. But it's not a toy. Some of the largest verification efforts have been done in Dafny. See e.g. IronFleet [1]. [1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf
  - gsbcbdjfncnjd 2y ago
    F* also uses SAT/SMT, specifically Z3.
    - nextos 2y ago
      Sure, what I meant is that Dafny outsources everything to SAT/SMT. If it doesn't manage to prove things for you, it gets a bit frustrating as there is not much support for manual tactics compared to F*, Coq or Isabelle, which can also leverage SAT/SMT, but have other options.
  - fovc 2y ago
    Agree it’s not a toy. AWS implemented a large chunk of IAM in Dafny. Though IIRC they have their own non-public compiler to Java
- deleted 2y ago
  [deleted]
markusde 2y ago
Do you think you might be able to elaborate a little bit more about this? I was skimming the "Proof-Oriented Programming" book, and it seems that the primary way to execute F* programs is by extraction or trusted compilation (same as Rocq and Lean, for example). Does F* have some special way to work directly with realistic source code that these other systems don't?
- seeknotfind 2y ago
  F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. In Coq, there's not a standard way to generate code, you might model and create code many different ways. F* seems to bring this in as the central goal of the language. So I'm discussing this structural difference. F* has an SMT solver, but Lean can import an SMT solver. So the goal is the important difference here - making theorem proving as accessible as possible in a real language. It's a move in the right direction, but we want to get to the point standard program languages have this support if you need it.
  - oisdk 2y ago
    > F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. Lean is also a programming language with proof support. It is very much in the same category as F* in this regard, and not in the same category as Coq (Rocq).
    - clarus 2y ago
      In Rocq/Coq, you have "extraction", which is the standard way to compile programs. This is how the C compiler CompCert is executed, for example. So, all of these languages are in the same category in this respect.
rajamaka 2y ago
Where would a smooth brained CRUD app web developer who failed high school maths perhaps learn more about the point of this?
- seeknotfind 2y ago
  The point would be to prove that your database stays consistent, a DB upgrade wouldn't break, or that you could achieve 100% up time given certain assumptions. An automated solver/prover might even be able to tell you where in your program breaks this. Without a technology like this, you have to carefully read your program, but this is the methodology to make the computer deal with that. Unfortunately formal verification is mostly used for research, F* is framing itself as taking a step to bring that to production codebases. Unfortunately I don't know good resources, but as researchers adapt this technology, and as we automate a lot of the heavy mathematics, you'd never want a programming language without this option.
nickpsecurity 2y ago
I’ll add that SPARK Ada allows this now, has commercial tooling from Adacore, and was field-prove in years of commercial deployments. https://en.m.wikipedia.org/wiki/SPARK_(programming_language) https://en.m.wikipedia.org/wiki/SPARK_(programming_language) It builds on the Why3 platform which also supports Frama-C for the C language. IIRC, SPARK can be compiled to C for C-only, runtime targets as well.
newpavlov 2y ago
>memory safe (without a borrow checker) This sounds like a very weird statement. In my opinion, a proper proof-oriented language would inevitably contain a borrow checker variant as a subset of its functionality (assuming the language has notion of pointers/references and focuses on achieving "zero cost abstractions"). Lifetime annotations and shared/exclusive references provide essential information and code use restrictions which enable automatic proof generation. After all, type and borrow checkers are nothing more than limited forms of automatic proof generation which are practical enough for wide use.
guerrilla 2y ago
> I 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. How does Idris compare these days?

akkad33 2y ago

https://dafny.org/ 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

nextos 2y ago
Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts). It's a great place to start with verification, as proofs are discharged to SAT/SMT, so things are automated. It can get a bit frustrating when automation is not able to prove things, that's the major disadvantage of SAT/SMT. But it's not a toy. Some of the largest verification efforts have been done in Dafny. See e.g. IronFleet [1]. [1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf
- gsbcbdjfncnjd 2y ago
  F* also uses SAT/SMT, specifically Z3.
  - nextos 2y ago
    Sure, what I meant is that Dafny outsources everything to SAT/SMT. If it doesn't manage to prove things for you, it gets a bit frustrating as there is not much support for manual tactics compared to F*, Coq or Isabelle, which can also leverage SAT/SMT, but have other options.
- fovc 2y ago
  Agree it’s not a toy. AWS implemented a large chunk of IAM in Dafny. Though IIRC they have their own non-public compiler to Java
deleted 2y ago
[deleted]

markusde 2y ago

Do you think you might be able to elaborate a little bit more about this? I was skimming the "Proof-Oriented Programming" book, and it seems that the primary way to execute F* programs is by extraction or trusted compilation (same as Rocq and Lean, for example). Does F* have some special way to work directly with realistic source code that these other systems don't?

seeknotfind 2y ago
F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. In Coq, there's not a standard way to generate code, you might model and create code many different ways. F* seems to bring this in as the central goal of the language. So I'm discussing this structural difference. F* has an SMT solver, but Lean can import an SMT solver. So the goal is the important difference here - making theorem proving as accessible as possible in a real language. It's a move in the right direction, but we want to get to the point standard program languages have this support if you need it.
- oisdk 2y ago
  > F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. Lean is also a programming language with proof support. It is very much in the same category as F* in this regard, and not in the same category as Coq (Rocq).
  - clarus 2y ago
    In Rocq/Coq, you have "extraction", which is the standard way to compile programs. This is how the C compiler CompCert is executed, for example. So, all of these languages are in the same category in this respect.

rajamaka 2y ago

Where would a smooth brained CRUD app web developer who failed high school maths perhaps learn more about the point of this?

seeknotfind 2y ago
The point would be to prove that your database stays consistent, a DB upgrade wouldn't break, or that you could achieve 100% up time given certain assumptions. An automated solver/prover might even be able to tell you where in your program breaks this. Without a technology like this, you have to carefully read your program, but this is the methodology to make the computer deal with that. Unfortunately formal verification is mostly used for research, F* is framing itself as taking a step to bring that to production codebases. Unfortunately I don't know good resources, but as researchers adapt this technology, and as we automate a lot of the heavy mathematics, you'd never want a programming language without this option.

nickpsecurity 2y ago

I’ll add that SPARK Ada allows this now, has commercial tooling from Adacore, and was field-prove in years of commercial deployments. https://en.m.wikipedia.org/wiki/SPARK_(programming_language) https://en.m.wikipedia.org/wiki/SPARK_(programming_language) It builds on the Why3 platform which also supports Frama-C for the C language. IIRC, SPARK can be compiled to C for C-only, runtime targets as well.

newpavlov 2y ago

>memory safe (without a borrow checker) This sounds like a very weird statement. In my opinion, a proper proof-oriented language would inevitably contain a borrow checker variant as a subset of its functionality (assuming the language has notion of pointers/references and focuses on achieving "zero cost abstractions"). Lifetime annotations and shared/exclusive references provide essential information and code use restrictions which enable automatic proof generation. After all, type and borrow checkers are nothing more than limited forms of automatic proof generation which are practical enough for wide use.

guerrilla 2y ago

> I 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. How does Idris compare these days?