11 ms·

Verified Programming in F*: A Tutorial

159 points by jstrieb 6y ago

dang 6y ago
If curious see also— related from 2016: https://news.ycombinator.com/item?id=10949288 https://news.ycombinator.com/item?id=10949288
yetkin 6y ago
"It will help if you are already familiar with functional programming languages in the ML family (e.g., OCaml, F#, Standard ML), or with Haskell—we provide a quick review of some basic concepts if you're a little rusty, but if you feel you need more background, there are many useful resources freely available on the web, e.g., Learn F#, F# for fun and profit, Introduction to Caml, the Real World OCaml book, or the OCaml MOOC." Isn't it yet another copy of OCAML? I think it shouldn't say familiar but something different. I really don't underestimate any effort to make OCAML available on dot-net, but referring to excellent OCAML books can't be explained by simple 'familiarity'...
- scscsc 6y ago
  You are probably thinking of F#, not F*. Very different languages.
  - studius 6y ago
    "Programs written in F* can be translated to OCaml, F#, and C for execution. ... The latest version of F* is written entirely in a common subset of F* and F#, and bootstraps in both OCaml and F#."[1] https://en.wikipedia.org/wiki/F*_(programming_language) https://en.wikipedia.org/wiki/F*_(programming_language)
    - travv0 6y ago
      I’m not sure what point you’re trying to make with that quote. The languages that F* can be compiled to and the ones it’s written in aren’t relevant to what was being discussed.
    - RobertKerans 6y ago
      Why is that relevant though? You could also write a version of (for example) Prolog or Forth or Lisp using OCaml that would compile to OCaml for execution. Doesn't mean any of those are OCaml. Coq isn't OCaml. Haxe isn't OCaml. The fact that F* is written in, uses a subset of the syntax of and can be compiled to F# (or OCaml) is an implementation detail, the language and the purpose of the language aren't to be OCaml/F#.
- vmchale 6y ago
  > Isn't it yet another copy of OCAML No, closer to ATS maybe?
tartrate 6y ago
How's the interop with .NET and C#?
- wisam 6y ago
  Are you thinking F#? I believe that other than being ML-like language and being developed jointly by Microsoft Research and Inria, F* has nothing to do with F# and .NET.
  - studius 6y ago
    "Programs written in F* can be translated to OCaml, F#, and C for execution. ... The latest version of F* is written entirely in a common subset of F* and F#, and bootstraps in both OCaml and F#."[1] [1]- https://en.wikipedia.org/wiki/F*_(programming_language) https://en.wikipedia.org/wiki/F*_(programming_language)
    - wisam 6y ago
      Thanks, I stand corrected.
  - tartrate 6y ago
    No I was just hoping it was connected somehow. I only found a single mention of .NET: > F* provides a facility to specify interfaces to external modules that are implemented elsewhere. For example, operations that perform file input/output are implemented by the operating system and made available to F* programs via the underlying framework, e.g., .NET or OCaml.
- indolering 6y ago
  AFAICT not great. It's an academic language and doesn't focus much on interop. The F# extraction system has been broken previously and I wouldn't recommend relying on F* for any commercial work unless you have a connection to the core development team.
keyle 6y ago
I'm confused. Is this either very new or very old? What's the context?
- mmoskal 6y ago
  F* primary aim is correctness - think something between Coq/LEAN/Isabelle and OCaml/F#. It uses a dependent type system to verify deep functional properties of programs (say that qsort actually sorts, or that a tree is balanced and implements a mathematical map). Typically such languages are more academic than F*.
  - wolfspider 6y ago
    I would also say take a look at Bosque it is also from the same camp as F* but much simpler to use Z3 with.
- Multicomp 6y ago
  i am not familiar with fstar. But I will try to provide some context badly so someone who does know it can correct me. Javascript is dynamically typed, and so has no type checking until runtime, you don't know whether a passed in parameter is a string or not until you try to use it. C# is statically typed, so the compiler knows whether something is a string when passed in at compile time, not making you wait until runtime. Ocaml/F# have a stronger type system than c#, so you get the compiler looking for you not only that something is a string, but that it is a named type like fifteenString, which is a string with a length of always 15 characters. F* takes this even further, where the compiler checks for you that you've passed in a fifteenString and that it matches criteria in its value like "starts with hello" or "does not contain bye". C# saves you from needing to check if a param is even a astring at runtime. F# additionally saves you from needing to check if it is null and 15 characters in length at runtime. F* additionally saves you needing to check its value starts with hello at runtime. Again this is a single language feature probably poorly explained!
  - jen20 6y ago
    The only difference between F# and C# with respect to the notion of a "type which represents a string of length 15" is the amount of code to do it - as described by Scott Wlaschin [1]. You could do the equivalent in C# too. I don't know if this is also the case in Ocaml, though. [1]: https://fsharpforfunandprofit.com/posts/designing-with-types-more-semantic-types/#modeling-constrained-strings-with-types https://fsharpforfunandprofit.com/posts/designing-with-types...
sdfjkl 6y ago
I find the syntax both terrible to read and terrible to write. Syntax is what I look at first with any unfamiliar programming language. The syntax is the UI of a language and if that's terrible, I won't enjoy using it.
- sanxiyn 6y ago
  Since syntax of F* looks okay to me, I am curious what particular points of syntax of F* you find terrible to read and write.
  - idnefju 6y ago
    In general I like ML based syntax, but Haskell using type signatures really helps read code easier. Wish other languages would adopt them
    - paavohtl 6y ago
      I don't understand this critique with regards to F*. As far as I can tell it has a type signature syntax that is very similar to Haskell, and is used extensively in the linked tutorial.
- haskellandchill 6y ago
  It's the ML family of languages syntax, very familiar if you've studied programming languages. Not sure what you can find terrible about it, it's a clean and minimal syntax.
- gameswithgo 6y ago
  people get used to syntaxes, by avoiding languages that don’t immediately appeal to your current syntactic preferences you are missing out on actual important and interesting ideas over triviality that would go away with familiarity
- dragonwriter 6y ago
  > I find the syntax both terrible to read and terrible to write. I don’t, but then I've spent time with a variety of languages that, like F*, are from the ML syntax family, and find that syntax quite comfortable. I can see why it would seem that way at first impression to someone who, for instance, has almost exclusively used languages with Algol-derived syntax (which is pretty common these days, since outside of Haskell from the ML family and Clojure from the Lisp family, most currently popular languages have Algol-derived syntax, or at least superficially Algol-like syntax.) > Syntax is what I look at first with any unfamiliar programming language. It's one of the things I look at early on, too, but it's also something I try to not to judge to firmly early on, because subjective view of syntax, like other UI impressions, is highly dependent on familiarity, and it takes a while to get past superficial similarity and dissimilarity to what one is used to and into any deeper strengths and weaknesses of the syntax (or other UI).
the_only_law 6y ago
I’ve recently had a interest in formal verification in regards to programming, but my background is so god awful I’m afraid to approach it. How does F* fair for beginners with little prior exposure?
- haskellandchill 6y ago
  This tutorial aims to be beginner friendly, assuming you have a background in functional programming. However the pace is very brisk and would serve better for an intermediate learner familiar with the concepts. As a practical tool it would not provide much unless you really know what you are doing and plan to leverage the use of SMT Solvers and code generation. You'd be better off with simpler and more focused learning materials. The Little Prover or Software Abstractions for example.
- ernst_klim 6y ago
  > but my background is so god awful I suggest you to read (or rather solve) this masterpiece https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
bibelo 6y ago
Who reads f * * * instead of f*?
estebarb 6y ago
F* is a great idea for writing libraries that cannot fail. But setting up the environment could be better documented.
co_dh 6y ago
Just joking: will the version 3 called f***? I like the language btw.
adsharma 6y ago
Also see: https://rise4fun.com/fstar/tutorial https://rise4fun.com/fstar/tutorial Even though this sounds like formal verification gobbledygook, there is some information of practical value there. How many JSON validators have you seen in python and javascript? Why can't the static type checkers like mypy and pyright do this for us? The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. So one creates a new class with a validate() method, which is completely unnecessary and doesn't protect you against integer overflows elsewhere in the code. F* and OCaml derivatives are our best hope in developing a type system which perform these types of common checks in one integrated framework via refinement types and dependent types. Hopefully, one day that work can hit mainstream languages like python, javascript and whatever ends up being the system programming language of choice replacing C in the coming years.
- com2kid 6y ago
  > The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. I am pretty sure Ada did that in the 80s. :) I get what you are saying, but the example you gave is a pretty trivial one that has been solved (although not implemented very often...) for awhile in more "regular" languages!
  - adsharma 6y ago
    I picked the trivial example on purpose to make the point that none of the top 5 programming languages do it, even if it was solved in the 80s. Recent languages like swift/kotlin (which I expect will see increased usage in coming years) seem to have ignored this area. https://github.com/peter-tomaselli/swift-refined/blob/master/Tests/RefinedTests/RefinedTests.swift https://github.com/peter-tomaselli/swift-refined/blob/master... https://discuss.kotlinlang.org/t/refinement-types/9753/19 https://discuss.kotlinlang.org/t/refinement-types/9753/19
    - 6y ago
gautv 6y ago
How does the language compare to a language like Idris ?

159 points by jstrieb 6y ago

dang 6y ago

If curious see also— related from 2016: https://news.ycombinator.com/item?id=10949288 https://news.ycombinator.com/item?id=10949288

yetkin 6y ago

"It will help if you are already familiar with functional programming languages in the ML family (e.g., OCaml, F#, Standard ML), or with Haskell—we provide a quick review of some basic concepts if you're a little rusty, but if you feel you need more background, there are many useful resources freely available on the web, e.g., Learn F#, F# for fun and profit, Introduction to Caml, the Real World OCaml book, or the OCaml MOOC." Isn't it yet another copy of OCAML? I think it shouldn't say familiar but something different. I really don't underestimate any effort to make OCAML available on dot-net, but referring to excellent OCAML books can't be explained by simple 'familiarity'...

scscsc 6y ago
You are probably thinking of F#, not F*. Very different languages.
- studius 6y ago
  "Programs written in F* can be translated to OCaml, F#, and C for execution. ... The latest version of F* is written entirely in a common subset of F* and F#, and bootstraps in both OCaml and F#."[1] https://en.wikipedia.org/wiki/F*_(programming_language) https://en.wikipedia.org/wiki/F*_(programming_language)
  - travv0 6y ago
    I’m not sure what point you’re trying to make with that quote. The languages that F* can be compiled to and the ones it’s written in aren’t relevant to what was being discussed.
  - RobertKerans 6y ago
    Why is that relevant though? You could also write a version of (for example) Prolog or Forth or Lisp using OCaml that would compile to OCaml for execution. Doesn't mean any of those are OCaml. Coq isn't OCaml. Haxe isn't OCaml. The fact that F* is written in, uses a subset of the syntax of and can be compiled to F# (or OCaml) is an implementation detail, the language and the purpose of the language aren't to be OCaml/F#.
vmchale 6y ago
> Isn't it yet another copy of OCAML No, closer to ATS maybe?

tartrate 6y ago

How's the interop with .NET and C#?

wisam 6y ago
Are you thinking F#? I believe that other than being ML-like language and being developed jointly by Microsoft Research and Inria, F* has nothing to do with F# and .NET.
- studius 6y ago
  "Programs written in F* can be translated to OCaml, F#, and C for execution. ... The latest version of F* is written entirely in a common subset of F* and F#, and bootstraps in both OCaml and F#."[1] [1]- https://en.wikipedia.org/wiki/F*_(programming_language) https://en.wikipedia.org/wiki/F*_(programming_language)
  - wisam 6y ago
    Thanks, I stand corrected.
- tartrate 6y ago
  No I was just hoping it was connected somehow. I only found a single mention of .NET: > F* provides a facility to specify interfaces to external modules that are implemented elsewhere. For example, operations that perform file input/output are implemented by the operating system and made available to F* programs via the underlying framework, e.g., .NET or OCaml.
indolering 6y ago
AFAICT not great. It's an academic language and doesn't focus much on interop. The F# extraction system has been broken previously and I wouldn't recommend relying on F* for any commercial work unless you have a connection to the core development team.

keyle 6y ago

I'm confused. Is this either very new or very old? What's the context?

mmoskal 6y ago
F* primary aim is correctness - think something between Coq/LEAN/Isabelle and OCaml/F#. It uses a dependent type system to verify deep functional properties of programs (say that qsort actually sorts, or that a tree is balanced and implements a mathematical map). Typically such languages are more academic than F*.
- wolfspider 6y ago
  I would also say take a look at Bosque it is also from the same camp as F* but much simpler to use Z3 with.
Multicomp 6y ago
i am not familiar with fstar. But I will try to provide some context badly so someone who does know it can correct me. Javascript is dynamically typed, and so has no type checking until runtime, you don't know whether a passed in parameter is a string or not until you try to use it. C# is statically typed, so the compiler knows whether something is a string when passed in at compile time, not making you wait until runtime. Ocaml/F# have a stronger type system than c#, so you get the compiler looking for you not only that something is a string, but that it is a named type like fifteenString, which is a string with a length of always 15 characters. F* takes this even further, where the compiler checks for you that you've passed in a fifteenString and that it matches criteria in its value like "starts with hello" or "does not contain bye". C# saves you from needing to check if a param is even a astring at runtime. F# additionally saves you from needing to check if it is null and 15 characters in length at runtime. F* additionally saves you needing to check its value starts with hello at runtime. Again this is a single language feature probably poorly explained!
- jen20 6y ago
  The only difference between F# and C# with respect to the notion of a "type which represents a string of length 15" is the amount of code to do it - as described by Scott Wlaschin [1]. You could do the equivalent in C# too. I don't know if this is also the case in Ocaml, though. [1]: https://fsharpforfunandprofit.com/posts/designing-with-types-more-semantic-types/#modeling-constrained-strings-with-types https://fsharpforfunandprofit.com/posts/designing-with-types...

sdfjkl 6y ago

I find the syntax both terrible to read and terrible to write. Syntax is what I look at first with any unfamiliar programming language. The syntax is the UI of a language and if that's terrible, I won't enjoy using it.

sanxiyn 6y ago
Since syntax of F* looks okay to me, I am curious what particular points of syntax of F* you find terrible to read and write.
- idnefju 6y ago
  In general I like ML based syntax, but Haskell using type signatures really helps read code easier. Wish other languages would adopt them
  - paavohtl 6y ago
    I don't understand this critique with regards to F*. As far as I can tell it has a type signature syntax that is very similar to Haskell, and is used extensively in the linked tutorial.
haskellandchill 6y ago
It's the ML family of languages syntax, very familiar if you've studied programming languages. Not sure what you can find terrible about it, it's a clean and minimal syntax.
gameswithgo 6y ago
people get used to syntaxes, by avoiding languages that don’t immediately appeal to your current syntactic preferences you are missing out on actual important and interesting ideas over triviality that would go away with familiarity
dragonwriter 6y ago
> I find the syntax both terrible to read and terrible to write. I don’t, but then I've spent time with a variety of languages that, like F*, are from the ML syntax family, and find that syntax quite comfortable. I can see why it would seem that way at first impression to someone who, for instance, has almost exclusively used languages with Algol-derived syntax (which is pretty common these days, since outside of Haskell from the ML family and Clojure from the Lisp family, most currently popular languages have Algol-derived syntax, or at least superficially Algol-like syntax.) > Syntax is what I look at first with any unfamiliar programming language. It's one of the things I look at early on, too, but it's also something I try to not to judge to firmly early on, because subjective view of syntax, like other UI impressions, is highly dependent on familiarity, and it takes a while to get past superficial similarity and dissimilarity to what one is used to and into any deeper strengths and weaknesses of the syntax (or other UI).

the_only_law 6y ago

I’ve recently had a interest in formal verification in regards to programming, but my background is so god awful I’m afraid to approach it. How does F* fair for beginners with little prior exposure?

haskellandchill 6y ago
This tutorial aims to be beginner friendly, assuming you have a background in functional programming. However the pace is very brisk and would serve better for an intermediate learner familiar with the concepts. As a practical tool it would not provide much unless you really know what you are doing and plan to leverage the use of SMT Solvers and code generation. You'd be better off with simpler and more focused learning materials. The Little Prover or Software Abstractions for example.
ernst_klim 6y ago
> but my background is so god awful I suggest you to read (or rather solve) this masterpiece https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/

bibelo 6y ago

Who reads f * * * instead of f*?

estebarb 6y ago

F* is a great idea for writing libraries that cannot fail. But setting up the environment could be better documented.

co_dh 6y ago

Just joking: will the version 3 called f***? I like the language btw.

adsharma 6y ago

Also see: https://rise4fun.com/fstar/tutorial https://rise4fun.com/fstar/tutorial Even though this sounds like formal verification gobbledygook, there is some information of practical value there. How many JSON validators have you seen in python and javascript? Why can't the static type checkers like mypy and pyright do this for us? The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. So one creates a new class with a validate() method, which is completely unnecessary and doesn't protect you against integer overflows elsewhere in the code. F* and OCaml derivatives are our best hope in developing a type system which perform these types of common checks in one integrated framework via refinement types and dependent types. Hopefully, one day that work can hit mainstream languages like python, javascript and whatever ends up being the system programming language of choice replacing C in the coming years.

com2kid 6y ago
> The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. I am pretty sure Ada did that in the 80s. :) I get what you are saying, but the example you gave is a pretty trivial one that has been solved (although not implemented very often...) for awhile in more "regular" languages!
- adsharma 6y ago
  I picked the trivial example on purpose to make the point that none of the top 5 programming languages do it, even if it was solved in the 80s. Recent languages like swift/kotlin (which I expect will see increased usage in coming years) seem to have ignored this area. https://github.com/peter-tomaselli/swift-refined/blob/master/Tests/RefinedTests/RefinedTests.swift https://github.com/peter-tomaselli/swift-refined/blob/master... https://discuss.kotlinlang.org/t/refinement-types/9753/19 https://discuss.kotlinlang.org/t/refinement-types/9753/19
  - 6y ago

gautv 6y ago

How does the language compare to a language like Idris ?