[HN Gopher] Verified Programming in F*: A Tutorial
___________________________________________________________________
Verified Programming in F*: A Tutorial
Author : jstrieb
Score : 144 points
Date : 2021-01-04 09:04 UTC (13 hours ago)
(HTM) web link (fstar-lang.org)
(TXT) w3m dump (fstar-lang.org)
| tartrate wrote:
| How's the interop with .NET and C#?
| wisam wrote:
| 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.
| tartrate wrote:
| 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.
| studius wrote:
| "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)
| wisam wrote:
| Thanks, I stand corrected.
| bibelo wrote:
| Who reads f * * * instead of f*?
| sdfjkl wrote:
| 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.
| dragonwriter wrote:
| > 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).
| gameswithgo wrote:
| 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
| amw-zero wrote:
| What's an example of a language with a good syntax?
| mhh__ wrote:
| I think Python (if nothing else) has good syntax. Forcing
| students not to write spaghetti is probably the only thing I
| actually like about python.
|
| I really like the philosophy behind Haskell, for example, but
| I really think it's syntax let's it down - it encourages very
| snippet-y programming which in turn means structure can be
| require parsing rather than glancing at and also variables
| name that are very short.
| sanxiyn wrote:
| 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 wrote:
| In general I like ML based syntax, but Haskell using type
| signatures really helps read code easier. Wish other
| languages would adopt them
| paavohtl wrote:
| 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 wrote:
| 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.
| dang wrote:
| If curious see also-- related from 2016:
| https://news.ycombinator.com/item?id=10949288
| co_dh wrote:
| Just joking: will the version 3 called f***? I like the
| language btw.
| the_only_law wrote:
| 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?
| ernst_klim wrote:
| > but my background is so god awful
|
| I suggest you to read (or rather solve) this masterpiece
|
| https://softwarefoundations.cis.upenn.edu/
| haskellandchill wrote:
| 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.
| yetkin wrote:
| "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'...
| vmchale wrote:
| > Isn't it yet another copy of OCAML
|
| No, closer to ATS maybe?
| scscsc wrote:
| You are probably thinking of F#, not F*. Very different
| languages.
| studius wrote:
| "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)
| travv0 wrote:
| 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 wrote:
| 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#.
| estebarb wrote:
| F* is a great idea for writing libraries that cannot fail. But
| setting up the environment could be better documented.
| adsharma wrote:
| Also see: 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.
| dragonwriter wrote:
| > 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?
|
| Because JSON is external data, mypy and pyright operate on
| Python code.
|
| > 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].
|
| Mypy can, in fact, do that (via a union of literal types),
| though the UX is horrible for that specific case and it only
| handles simple literals, but that's actually enough for JSON
| semantics. Of course, to validate JSON with it, you'd have to
| turn the JSON into Python code with type annotations and
| validate that.
| com2kid wrote:
| > 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 wrote:
| 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...
| https://discuss.kotlinlang.org/t/refinement-types/9753/19
| ampdepolymerase wrote:
| Because it requires a non-trivial amount of static analysis
| work on the compiler side to make the UX comfortable.
| Rust's borrow checker mechanism took years to become
| pleasant for the end user to use. There is still next to no
| adoption of Ada outside of aerospace, defence, and certain
| embedded programming sectors.
| com2kid wrote:
| It is super annoying that it isn't done more.
|
| I'd love to be able to opt in to bounds checking when I
| feel it is needed.
|
| I have no bloody idea why language designers seem so intent
| on not letting me choose what perf/safety trade-off is
| worthwhile for me. :/
| pjmlp wrote:
| Easy, use C++.
|
| While not perfect, given its copy-paste compatibility
| with C, you can opt-in into bounds checking by using the
| STL data types, or similar.
|
| Then you can also make use of compiler switches, to opt-
| in in changing the behaviour of operator[]() to do bounds
| checking.
|
| With templates, you can opt-in into checked numerics.
|
| While not perfect, and maybe it will be replaced by Rust
| or other candidate someday, it already offered plenty of
| opt-in possiblities since early 90's, no need to keep
| writing C.
| z3t4 wrote:
| Type systems do not thinking for you, you still have to make a
| type with a range check. So you could just as well write
| function foo(n) { if(n < 10 || n > 100) throw new
| Error("Expected n=" + n + " to be between 10 and 100");
| return n*2; }
|
| And while you are at it you can write an unit test that is
| tested at compile time or in the editor/IDE. //
| assert(foo(10),20);
| amw-zero wrote:
| Try reading the tutorial. F* uses refinement types, which
| means that logic is checked before the program is executed,
| at compile time.
| keyle wrote:
| I'm confused. Is this either very new or very old? What's the
| context?
| sradman wrote:
| According to the F* landing page [1]:
|
| > F* (pronounced F star) is a general-purpose functional
| programming language with effects aimed at program
| verification.
|
| > The main ongoing use case of F* is building a verified, drop-
| in replacement for the whole HTTPS stack in Project Everest
| [2]. This includes verified implementations of TLS 1.2 and 1.3
| and of the underlying cryptographic primitives.
|
| [1] http://www.fstar-lang.org/
|
| [2] https://project-everest.github.io/
| mmoskal wrote:
| 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 wrote:
| 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.
| vmchale wrote:
| Fairly new language.
| ivarru wrote:
| As pointed out by dang, the same (I think) tutorial was
| discussed in 2016
| (https://news.ycombinator.com/item?id=10949288). I went through
| the first half of the tutorial in 2018, and I think some
| aspects of F* were genuinely new, but the development seems to
| have stopped. There is a need for a framework for program
| verification of real-life software by non-experts, but F* might
| not be it. In the latest article [1] of Project Everest one can
| read: "[...], it required several person-months to implement
| and verify a generic doubly-linked list library in F*, while it
| required only three hours to do so in Dafny."
|
| [1] A Security Model and Fully Verified Implementation for the
| IETF QUIC Record Layer (Antoine Delignat-Lavaud, Cedric
| Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro,
| Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou)
| To Appear In The Proceedings of the 42nd IEEE Symposium on
| Security & Privacy 2021.
| brundolf wrote:
| it required several person-months to implement and verify a
| generic doubly-linked list library in F*, while it required
| only three hours to do so in Dafny
|
| This could be deceptive. Structures like linked-lists are
| fiendishly hard to implement in safe Rust too, but people are
| able to stay productive by (mostly) not implementing things
| like that themselves. In Rust's case the difficulty comes
| from ownership: anything involving complex reference graphs
| for the sake of traversal is going to be really gnarly to
| establish a single-ownership story for. I don't know about
| F*.
| Multicomp wrote:
| 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!
| globuous wrote:
| Ocaml beginner here, didn't know you could restrict an Ocaml
| type to a string of a given length !! How would you go about
| that ?? Cheers :)
| jen20 wrote:
| 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...
| gautv wrote:
| How does the language compare to a language like Idris ?
___________________________________________________________________
(page generated 2021-01-04 23:01 UTC)