F* – An ML-like functional programming language aimed at program verification
fstar-lang.org
fstar-lang.org
"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."
[1] Modulo things like the correctness of their C semantics, assembly semantics, various extraction procedures.
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.
I wish they at least named it Fasterisk
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.
But (for example, for a web server written in Ada or C) you can also do without a specification and just apply verification tools to only check things like "all memory accesses are valid", proving that you have no buffer overflows that would cause denial of service or security holes.
Of course someone still has to write the verification tool correctly to ensure that it actually gives the safety guarantees you want, but at least it's not you who has to worry about that ;-) And specifying the absence of buffer overflows is comparatively simple.
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.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
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.
[1]: http://gigiigig.github.io/tlp-step-by-step/dependent-types.h...
[2]: https://www.reddit.com/r/cpp/comments/2tilfw/dependent_typin...
Which function in there do you consider to have a return type that depends on the value of the input?
In that case, it may be even more puzzling to claim that C++ has dependent types.
Checking refinements at run time is considered "too expensive" by many people.
The big win with refined types is from compiler level support though. With relatively simple checking occurring mostly at IO boundaries, you can eliminate or make obsolete massive portions of testing, type checking, manual optimization, etc., and enable massive amounts of automated optimization. In other words, the "too expensive" refinement checking at runtime becomes a net performance and engineering benefit over the whole product lifecycle.
Better quality of software is irrelevant unless they get fined, like it happens on medicine or aeronautics industry.
They only care about cost centers, Excel reports and who delivers at lower cost per seat.
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.
"Type system tyranny", page 8 - 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."
The real question is, why can they afford to take this approach without being outperformed by companies that use better languages and better developers?
For those of us who enjoy exploring more powerful/innovative languages, there is a convenient explanation and a not so convenient explanation.
The convenient one is that the success of these "Blub companies" is largely determined by factors unrelated to software development.
The inconvenient one is that all these interesting and powerful language features do not significantly improve software development outcomes.
I think it is remarkable that some of the companies that are on the Blub side when it comes to software development are among the most cutting edge, research oriented companies in other regards, such as AI.
Also, companies like Google can not only choose among the best candidates, they also have a lot of influence on what people learn before they even apply for a job there. So I simply don't buy the familiarity excuse, at least not for the entire workforce.
I also don't buy the large existing codebase excuse as that would apply equally to new Blub languages and new PL research based languages.
There is simply very little faith in any positive impact of PL research innovations on software development outcomes. And this lack of faith cannot be explained away by claiming that all those lacking faith are simply incompetent.
The likes of Google and Microsoft can and do hire competent PL researchers, just as they hire competent AI researchers. And they do have a massive incentive to improve software development quality and productivity.
I think the truth is that PL researchers simply haven't made the case for the effectiveness of their work.
In part because it's extremely difficult to make that case empirically. All the empirical studies I have seen suffer from huge and mostly unfixable counfounders.
But I think another reason is that PL researchers seem to largely ignore cognitive science and sociology. I haven't seen much discussion about the impact of particular PL features on developers' state of mind in any realistic context.
Nor have I seen much debate about programming languages as group communication tools or about the different roles in which people interact with code as part of a software development process. All of that is apparently considered out of scope.
And that, I think, is the reason why it is so easy for many practitioners to dismiss PL research out of hand. Even where PL research is being picked up decades later it appears more fashion driven than evidence based.
Yet, most likely we would use heavy construction building machines nowadays.
Niklaus Wirth admits on one of his papers that he expected developers would pick Oberon by caring about tools for quality in software engineered, but he was wrong about it.
Hoare has a similar remark on his Turing award speech.
So from my point of view it is a mix of sociology, fashion driven development and office politics.
If so, you must be very confused with what they are doing with Go and Swift and Dart if you still consider that a thing.
type Int is range 0 .. 100;
type Int is range 0 .. 100 check(v)
if (v = 10) or (v = 50) then error;
end;
type Foo = object
Enabled : Boolean; Magnitude : 0..1000;
check
if (Enabled and (Magnitude=0)) or
(not Enabled and (Magnitude > 0)) then error;
end;
procedure Bar;
end;
Or at least that is what i remember understanding.
Maybe i remember some other Pascal-styled language, but the only other such language i know of is Oberon and that goes against the "put everything imaginable, plus extra more" mentality of Ada seems to have :-P.
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.
Also compared with Coq, proofs rely heavily on SMT solving with Z3 instead of lots of manual tactics (yay!). On the other hand, where SMT solving fails, you can not resort to manual tactics because there is no tactic language. You have to write proof terms without interactive support. (This may have changed in the last few months, but I'm almost sure it hasn't.)
I wrote a bit about my experiences trying to prove things in F* two years ago: https://news.ycombinator.com/item?id=10984306
Don't rely on any of that though, things will have changed in the meantime!
I'm optimistic about F*, but at the moment you have to be quite determined to try to use it for fully verified programming. The same is true for Coq, though.
We've been mostly studying hammer-like tactics to, say, apply some theorems at specific places in the goal (which the SMT might be bad at), and not for chaining small rewriting or logical steps (which the SMT is good at).
Stopping short of full end-to-end functional correctness, there are lot more notable examples, such as the Verve system at MSR (verified type/memory safety using Boogie), and the Bedrock system at MIT (functional correctness down to a fairly low-level IR, done in Coq), the miTLS/Everest TLS stack (protocol correctness verified in F-star, most of the way down to a C-like implementation), and the Iris project (a toolkit for verifying higher-order concurrent programs, currently being used to formalize Rust including unsafe, in Coq).
In machine-checked proof, the three biggest successes are the verification of the Odd Order Theorem (in Coq), the Four Colour Theorem (in Coq), and the Flyspeck project verifying the proof of the Kepler conjecture (in HOL).
In hardware verification, there has been a huge amount of work using ACL2 and HOL, but I don't know this space as well.
Basically, Coq and Isabelle have the most actual successes, but other things like F-star, Boogie and HOL have all worked as well.
For example, I wouldn't want to try to write the kind of fiddling with byte arrays involved in cryptography in Coq. F* is certainly better for that. I imagine Dafny is better for it, too. Possibly Why3 as well. Or, if that is really what you want, you might even go for "real" programming languages (ones that exist independently of verification frameworks) such as Ada with SPARK/Ada or C with Frama-C.
If you want to verify purely functional programs, Coq is pretty good, but proving is often boringly manual. Also, the language is more influenced by the OCaml branch of the ML family than by Haskell; for Haskellers there are Idris and Agda. Then there is Isabelle/HOL, which has a lot of proof automation but a bizarre logic.
Oh, I haven't even mentioned Lean. Well. There is really no easy answer: You have to try to get acquainted with several of the frameworks, ideally with an idea for what your application will be. And whichever you choose, it will be hard.
https://maniagnosis.crsr.net/tags/applied%20formal%20logic.h...
That said, I think the thing that annoyed me most were the different language levels: "assume P show Q" and "P ==> Q" are both implications, but somehow different. I never quite understood why and how, but there seem to be cases where only one can be proved but not the other. Similarly for different kinds of universal quantification. Your interpretation of "bizarre" may very well vary, but I found these unintuitive and not explained well in the documentation that I found.
(Don't ask for anything much more concrete than this. It's been a while, and I've forgotten the details.)
FWIW the differences are largely syntactic. Some of them are due to implication or quantification being in the meta-level (Pure, Λ/long ⇒) vs object-level (HOL, ∀/⟶). Transporting between them (for HOL) is easy and the automation tends to normalize object-level quantification and implication into meta-level.
"assume P show Q" is just Isar-syntax for a structured proof of "P ==> Q" (which is a term).
https://www.amazon.com/Building-High-Integrity-Applications-...
Verification of larger programs is hard for a lot of reasons. Easiest method is to do Design-by-Contract in a memory-safe language. Anything easy to specify in contracts goes there where stuff easier to test for is done that way. If your language doesn't support it, you can do it with asserts, conditionals in functions, or constructors/destructors in OOP.
http://www.eiffel.com/developers/design_by_contract_in_detai...
Then, you hit the app with tests generated from the contracts and fuzz testing that both run while the contract conditions have runtime checks in the code. That means a failure will take you right to the precondition, invariant, or post condition that is broken.
For analyzing distributed stuff, TLA+ is your best bet with an accessible tutorial for a subset available here:
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.