1. 15

  2. 6

    Interesting development. COGENT already did verification of functional programs that translate to C or assembly. This is Everest’s take on these things doing F star to C compiler. This is significant given they’re doing a verified TLS stack in F star. Anyone not into functional programming or formal methods should skip straight to the F star and C implementations of Chacha20 in the article. The F star code is amazingly readable with the C code more readable than many crypto implementations I’ve seen despite being mechanically generated. Code often designed for easy verification by humans or machines. Rare to see projects whose code does great on both.

    1. 1

      other than crypto, are there any compelling uses for this (versus just writing code in ocaml)?

      1. 4

        F* has a stronger type system than F#/OCaml. Here are some of the type system features:

        F* (pronounced F star) is an ML-like functional programming language aimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs.


        It also has multiple compilation targets. Initially F* could compile to F# or OCaml. Later the Javascript backend was added (although it looks like that has been dropped), and now they’ve added C.

        1. 1

          the bit i’m having trouble with is, for what sort of programs does the stronger type system really help me? e.g. i can think of use cases for languages like rust, eff and even ats, all of which extend the ML type system to solve problems that i can relate to, but f* seems very geared towards things like crypto and security, and not so much to writing userland apps.

          1. 2

            I haven’t heard of EFF outside the Electronic Frontier Foundation, what is that?

            Stronger type systems help to produce more reliable, guarantee-able software in general. This is especially helpful for crypto and security, but you should be able to reap the benefits anywhere. Constraints make systems more predictable.

            Granted, linear/affine types in a language like Rust have a very explicit advantage - deterministic, automatic memory management. The case for dependent types or refinement types isn’t as snazzy, but they do help constrain system behavior.

            I tried to use ATS about a year ago, and imho the language is too inscrutable. It has an impressive type system, but the arbitrary style decisions are too much for me to stomach. Look at the examples on the wiki page to get a sense of what I mean: strange keywords like t@ype, and four different file extensions cats, dats, hats, and sats. The syntax is ML-inspired but very bizarre.

            Now that F* can compile to C, it may be able to fill the niche of “more usable ATS”.

            1. 1

              this eff: http://www.eff-lang.org/

              also i agree with you about ATS - i really want to like it, but it’s just too inscrutable. however, F* doesn’t have linear types, does it? that was the main reason i got interested in ATS, so i see rust rather than F* as the “more usable ATS”. (If F* does have linear types i missed it in the tutorial). The most personally interesting thing i saw in F* was the idea of refinement types, but I’m currently shying away from having to learn a whole proof system and dependently typed language just to get those.

              1. 3

                I think F* actually does have affine types. I was able to search for the term in this pdf: http://research.microsoft.com/en-us/um/people/nswamy/papers/fstar-jfp.pdf

                However, the language was originally designed to target F# and OCaml, so I’m not sure how easy it will be to avoid garbage collection. KreMLin seems to imply that the C transpiler does not work on all F* programs:

                the [transformed] code ends up in a limited, first-order, monomorphic subset of F* called Low*. If code falls within the Low* subset, then KreMLin knows how to translate it to C.