11 ms·
F* – An ML-like functional programming language aimed at program verification
- make3 9y ago...it's unfortunate the name kinda looks like a censored bad word
- quickthrower2 9y agoIt's compatiable with Coq
- deleted 9y ago[deleted]
- smsm42 9y agoWhat is it with this trend of giving languages unsearchable names?
- divanvisagie 9y agoIt's only a problem if you use it.
- viach 9y agoSearching for "f*" gives correct link in 1st result in Google. Do you use Yahoo or other search engine?
- ainar-g 9y agoI am not the other person, but when I try to find a JSON decoding module for F* with "f* json", I get almost completely unrelated results. So, either there is no JSON codec for F* (I guess they could use the F#'s one) or Google can't find it.
- arkkh 9y agoyou would just type "fstar json" instead, just like you'd type "fsharp" instead of "f#"
- smsm42 9y agoDDG (which I use) doesn't.
- Myrmornis 9y agoI agree, I used to use R and found it hard to google for.
- cschmidt 9y agohttp://rseek.org/ http://rseek.org/ is a specialized R search engine, only necessary due to the name
- maxxxxx 9y agoThis actually is a real problem. Searching for "C#", "F#" or ".NET" breaks a lot of search engines and you get nothing useful. If I had to name something now I would go for a relatively unique name like "Clojure", "TypeScript" or "Haskell".
- ainar-g 9y agoWhy didn't refinement types find their way into mainstream languages yet? It seems like it would have a tremendous impact on how programs are written and tested.
- pjmlp 9y agoBecause major organizations only want replaceable developers, as cogs in the enterprise machine. Better quality of software is irrelevant unless they get fined, like it happens on medicine or aeronautics industry.
- ainar-g 9y agoIf anything, I would say refinement types make developers more replaceable. If Developer-1 documents all assumptions in the code using refinements, then, when they are replaced with Developer-2, the new developer can be productive more quickly.
- pjmlp 9y agoI agree with you, but most managers don't. They only care about cost centers, Excel reports and who delivers at lower cost per seat.
- kakarot 9y agoThose "major organizations", with the exception of Google and Apple, aren't spearheading language design. Their point of view has no impact on the evolution of language paradigms, and if you told them they could save money on QA and increase the reliability of their product for virtually no overhead with new paradigms, I don't see why many people would reject the idea.
- pjmlp 9y agoGoogle, as in Go? "Type system tyranny", page 8 - https://talks.golang.org/2009/go_talk-20091030.pdf https://talks.golang.org/2009/go_talk-20091030.pdf "Programmers working at Google are early in their careers and are most familiar with procedural languages, particularly from the C family. The need to get programmers productive quickly in a new language means that the language cannot be too radical." https://talks.golang.org/2012/splash.article https://talks.golang.org/2012/splash.article
- fsloth 9y agoHow does this compare with other verification tools such as TLA+ or Coq?
- ahelwer 9y agoTLA+ is a specification language, not a verification language. There is currently no way of establishing correspondence between a TLA+ spec and the code you (presumably) write to implement that spec. There are benefits to this, like using TLA+ to spec the difficult parts of your system without having to buy the whole formal verification farm.
- pron 9y agoNot just that. F* is convenient for code-level specification, much like Ada SPARK, JML/OpenJML for Java, and ACSL/Frama-C for C, but it's quite hard to specify global correctness conditions in it, like "the database is always consistent", or "no data is ever lost", which is where TLA+ shines. The gap between local, code-level correctness properties and global ones is a hard one to cross. I am not aware of any tool that can do both (i.e. end-to-end verification) in a way that isn't excruciatingly hard.
- hwayne 9y agoAnd not just _that_, but TLA+ is really good at expressing liveness conditions, like "the database is EVENTUALLY consistent" or "the algorithm will eventually terminate." Most other formal methods don't cover that.
- pron 9y agoRight; not out of the box, anyway (many proof assistants are powerful enough for deep embedding of arbitrary logics, but, of course, using them is beyond the affordable reach of nearly all software shops). Many can express termination out of the box, which, in theory, can suffice to express most (all?) liveness properties, certainly many useful ones, but again, this is expressed at the function level, and hard to do for global liveness properties.
- ZenoArrow 9y agoIn terms of buzzword bingo, F* is as close to my ideal programming language as I can think of, but I do wonder if it'll ever get the tooling support to make it more attractive as a general purpose language.
- tytytytytytytyt 9y agoWhat is it missing that something like SML has? Why couldn't I just switch from another language to this today, assuming I don't care about IDE support for it?
- ZenoArrow 9y agoIf you're interested, and you don't care much about tooling, go for it: https://github.com/FStarLang/FStar/blob/master/INSTALL.md https://github.com/FStarLang/FStar/blob/master/INSTALL.md
- philonoist 9y agoOne thing I am amused is the behemoth support by Microsoft Research. Why is it still dormant? https://www.microsoft.com/en-us/research/project/the-f-project/ https://www.microsoft.com/en-us/research/project/the-f-proje... https://en.wikipedia.org/wiki/F*_(programming_language) https://en.wikipedia.org/wiki/F*_(programming_language)
- foota 9y agoMaybe they're looking to improve the developer experience? Seems like f# took a long time before entering the spotlight as well.
- tom_mellior 9y agoMicrosoft Research is also behind Dafny and Lean and a whole bunch of more specialized tools: https://rise4fun.com/ https://rise4fun.com/ They are very wisely not claiming that any of these is the verified programming language to rule them all. There is still a lot to learn.
- Jaxan 9y agoA nice project using F* is the project Everest: https://project-everest.github.io https://project-everest.github.io . They implement HTTPS and all of its crypto, completely verified.
- qualitytime 9y ago"Current status - We generate a C library, but the verification is not complete."
- tom_mellior 9y agoNote however that the page does list a bunch of useful, completely[1] verified components just below that sentence. [1] Modulo things like the correctness of their C semantics, assembly semantics, various extraction procedures.
- catalin_hritcu 9y agoOne can always look at the empty part of the glass, but the quote does continue with a big full part: "The TLS 1.3 handshake verification is work in progress and still relies on the OCaml extraction mechanism of F* ; thus, the C library still encapsulates the OCaml runtime system. We have completed verification of the TLS 1.3 record layer it currently extracts to C. The AES and SHA2 cryptographic assembly routines are verified and extract to assembly via Vale. HaCl* provides verified C code for multiple other primitives such as Curve25519, Chacha20, Poly1305 or HMAC. Our test client implements TLS 1.2 + TLS 1.3 Draft 18 and successfully connects to TLS 1.3 test servers. We have a prototype integration of miTLS within libcurl that one can use to git clone a remote repository."
- sitkack 9y agoVs the pile that is OpenSSL.
- ernst_klim 9y agoI've always dreamed about ML language with verification support and dependent types. Does it have something like Haskell's typeclasses or OCaml's modular implicits? Does it support ad-hoc polymorphism in any way?
- lmm 9y agoWhat do you think of Idris?
- olzd 9y agoIdris certainly is nice but I doubt anyone uses it for real stuff.
- hiker 9y agoLean is quite nice dependently typed language https://leanprover.github.io/ https://leanprover.github.io/
- saosebastiao 9y agoIt's not intending to be a general purpose language, and as such doesn't have a lot of features that make software engineering easier. In fact, it intentionally has a phenomenally slow compiler, because the compiler is solving or attempting to solve various NP-Complete problems simultaneously. Think of it as a language that will help build tools, analyzers, and possibly linkable libraries for small scale but highly security-critical components, but not necessarily the language you want to use to build an app server.
- platz 9y agoalthough, if you don't use any refinement types in your program, i don't see why you can't write general purpose programs and extract code to Ocaml and F#
- infruset 9y agoThis post describes how Mozilla is incorporating F* verified cryptographic code into Firefox: https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/ https://blog.mozilla.org/security/2017/09/13/verified-crypto...
- BLanen 9y agoMaking another new language with such a short un-search-enginable name is not a good idea imo.
- abrookewood 9y agoWell, type "f*" into Google and it's the second result ... Why Facebook is first, I have no idea.
- splintercell 9y agoI believe that Google might have created a rule for that, because when you type this in Yahoo [1] (or I believe even Solr, ElasticSearch or any of the other full text based database search engines) you won't find this as a result. 1. https://search.yahoo.com/search?ei=UTF-8&fr=crmas&p=f* https://search.yahoo.com/search?ei=UTF-8&fr=crmas&p=f*
- jonwinstanley 9y agoWhy was it not named FML?
- beurdouche 9y agoOne cool thing with F* is that it starts bringing real contributions such as the HACL* formally verified cryptography to Firefox. https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/ https://blog.mozilla.org/security/2017/09/13/verified-crypto... Realistically, even if F* is not fully foundational it seems to be a very good compromise to write security sensitive applications in terms of proof effort...
- corey_moncure 9y agoIs it easier to write a program that behaves the way you want and a verification to prove the program behaves the way you want, or to just write the program? What if you goofed writing the verification, and now you have a program that is guaranteed to misbehave? How do you verify the verification?
- cmrx64 9y agoValidation vs verification. Validation: "is this the right spec", verification: "does this meet the spec". Turns out once you have a formal specification, you can do all sorts of things with it that you couldn't do with just the code sitting alone. You can prove properties about your specification. For example, seL4. Even the abstract specification is quite big and can be hard to reason about in complex cases. How do you know that spec is the one you want? Well, they wrote down some security properties they'd like it to have, and then proved that the abstract spec has those properties (eg, you can configure it to act like a separation kernel; it enforces isolation given an isolated initial condition; it enforces integrity). How do you know those are the right properties? Well, that's the challenge of software validation isn't it :) Ultimately formal methods doesn't make that problem much harder. You just need to figure out a way to formally phrase the properties you want. A lot of software has very fuzzy validation criteria, and isn't necessarily suited for formal verification for that reason.
- throwawayjava 9y ago> How do you verify the verification? https://mathoverflow.net/a/18436 https://mathoverflow.net/a/18436
- nickpsecurity 9y agocmrx64 addressed the validation well. I'll add that there's formal specification tools for requirements (the What) such as Software Cost Reduction and Abstract, State Machines that have helped there. The trick on those is they help be precise about the environment, inputs, and outputs in a way human reviewers can understand. So, the reviewers think on and discuss stuff with their thoughts shared to others in English and the formalism to spot the problems or even improvement opportunities. The main gotcha there is ensuring English and formal specs don't diverge. Far as verified stacks, the throwaway linked the basic concept but here's two works (old and new) on verified provers so you can see it in action: https://www.cs.princeton.edu/~appel/papers/flit.pdf https://www.cs.princeton.edu/~appel/papers/flit.pdf https://www.cs.utexas.edu/users/jared/milawa/Web/ https://www.cs.utexas.edu/users/jared/milawa/Web/ The former was early work by Appel et al on getting the TCB of provers down to a few thousand lines of code. The other uses composable logics and small implementation that itself uses the verified tooling of Myreen et al whose research covers a lot of angles: https://www.cl.cam.ac.uk/~mom22/research.html https://www.cl.cam.ac.uk/~mom22/research.html Most of their work is done in Isabelle/HOL which HOL/Light is aiming to verify in a lightweight way. The idea being you just have to trust the code of the kernel (hundreds to thousands of lines) that checks proof terms and the specs that are fed into them. They're doing everything they can in the proof assistants so the minimal checkers will be able to confirm the operations.
- 7kmph 9y agoCan't wait to see someone write some kind of checking program with the name F*ck.