jroesch

There have already been two file system verification projects, this year's OSDI best paper is the most recent example, http://locore.cs.washington.edu/papers/sigurbjarnarson-yggdr..., and last year as SOSP FSCQ: http://sigops.org/sosp/sosp15/current/2015-Monterey/013-chen...

Yeah I think SMT is really the state-of-the-art right now in this area. Leo De Moura (one of the main authors of Z3) has been working on Lean for the past couple of years. There is a small group of us (5~) who have been working on a big release for the past couple of months. The goal is to bring the easy of use of SMT automation to type theory, so you can get both the ability to do induction and automation.

Lean: http://leanprover.github.io/

A short answer is that the theory is just simpler. Non-dependent type theory spends a lot of effort separating values, types, kinds and valid operations over them. For example you need lots of extensions to make it possible to use a type both at the value, type, and kind level in Haskell. Each extension to the type system adds more complexity, and requires special code to implement its functionality (DataKinds, PolyKinds, TypeFamilies, etc). You also end up needing at least two or more different kinds of ASTs one that describes expressions, one for types, one for kinds, etc.

All of this falls away in dependent type theory you can represent the whole language with a class of pesudo-terms. For example the core expressions can be captured by the below grammar:

    term := x
         | f x
         | forall (x : Type), B x
         | lambda (x : A), e
         | Type

Type checking (not inference) is straight forward to implement for these theories and can be done in about a page or two of code. Of course "elaboration" or "type-inference" for these theories can be much more complex, but Haskell's isn't simple either. The most recent publication on the TI algorithm is roughly 80 pages.

The core theory (and implementation) is much simpler for almost all dependent type theories. At least this is my personal feeling after having read a lot of GHC code, written an Idris backend, the native backend for Lean, and significant portions of `rustc`.

Type inference isn't the most important, most languages that employ type inference are moving towards features sets make full inference hard, if not impossible. Not to mention you can get pretty good "inference" in dependently typed programming languages just by designing an appropriate higher order unification procedure. I have never met a daily user of these tools that find this to be the bottleneck.

In practice you spend way more time writing proofs in these system then doing anything else. There is evidence that we don't need to limit the expressive power of our logics, just design appropriate automation for the logic. Lean, a new ITT based theorem prover from MSR, has been focused on building automation for type theory. It already has promising results that formal methods techniques can be scaled to type theory (see the website for more information on recent work).

You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example there was a line of work in ACL2 that verified a microprocessor implementation, as well as plenty of modern work using tools like SMT to automatically prove program properties, see Dafny, F* for language based approaches. Though there is plenty of language agnostic approaches as well. My colleagues at UW have a paper in this year's OSDI verifying crash consistency for a realistic file system with no manual proof.

The problem with an optimization like this is that the current approach always gives you a guarantee on runtime cost. Heuristic based optimizations make performance harder to ensure, not to mention recovering performance when you fall outside the valid subset much more difficult. You can obviously provide another static analysis to warn you about violations, but this seems is more complex, and less flexible then the current approach.

I feel like you have confused quite a few concepts here.

First, type theory based proof assistants (like Coq) and model checkers are very different tools with very different guarantees. Most model checkers are used for proving properties about finite models and can not reason about infinite structures.

A type theory with inductive types gives one a mechanism for constructing inductive structures, and the ability to write proofs about them.

I am not sure how you have equated denotational semantics and type theory but there is no inherent connection, denotational semantics are just one way to give a language semantics. One can use them to describe the computational behavior of your type theory, but they are not fundamental.

Category theory and type theory have a cool isomorphism between them, but otherwise can be completely silo'd you can be quite proficient in type theory and never touch or understand any category theory at all.

On the subject of TLA+, Leslie Lamport loves to talk about "ordinary mathematics" but he just chose a different foundational mathematics to build his tool with, type theory is an alternative formulation in this regard. One that is superior in some ways since the language for proof, and programming is one and the same and does not require strange stratification or layering of specification and implementation languages.

Another issue with many of these model based tools is the so called "formality gap" building a clean model of your program and then proving properties is nice, but without a connection to your implementation the exercise has questionable value. Sure, with distributed systems for example, writing out a model of your protocol can help find design bugs, but it will not stop you from incorrectly implementing said protocol. In the distributed systems even with testing, finding safety violations in practice is hard, and many of them can occur silently.

Proof assistants like Coq make doing this easier since your implementation and proof live side by side, and you can reason directly about your implementation instead of a model. If you don't like dependently typed functional languages you can check out tools like Dafny which provide a similar work style, but with more automation and imperative programming constructs.

> This formulation serves as the basis for most formal reasoning of computer programs.

On this statement I'm not sure what community you come from, but much of the work going on in the research community is using things like SMT which exposes SAT and a flavor of first order logic, an HOL based system like Isabelle, or type theory, very few people use tools like set theory to reason about programs.

> Engineers, however, already have nearly all the math they need to reason about programs and algorithm in the common mathematical way (they just may not know it, which is why I so obnoxiously bring it up whenever I can, to offset the notion that is way overrepresented here on HN that believes that "PFP is the way to mathematically reason about programs".

Finally this statement is just plain not true, abstractly its easy to hand way on paper about the correctness of your algorithm. I encourage you to show me the average engineer who can pick up a program and prove non-trivial properties about its implementation, even on paper. I wager even proving the implementation of merge sort correct would prove too much. I've spent the last year implementing real, low-level systems using type theory, and this stuff is hard if you can show me a silver bullet I would be ecstatic, but any approach with as much power and flexibility is at least as hard to use.

Its not that "PFP" (and its not PFP, its type theory that makes this possible) is the "right way" to reason about programs but that it makes it possible to reason about programs. For example, how do you prove a loop invariant in Python? how would you even start? I know of a few ways to do this, but most provide a weaker guarantee then you would type theory version would, and requires a large trusted computing base.

At least in programming languages, systems, and formal verification project code is both available and often evaluated along side the publication. For example FSCQ(https://github.com/mit-pdos/fscq-impl) from MIT, Verdi (https://github.com/uwplse/verdi) from UW, Dune(http://dune.scs.stanford.edu/) from Stanford, and many more.

These are just the areas I work in, its very hard to making sweeping statement about CS as a full field since it is very diverse sub-community to sub-community.

I think they made a much better decision then everyone else even if verbose.

Nearly every language has continued to repeat Tony Hoare's "billion dollar" mistake of allowing null to inhabit any type. I think approaches like Rust's and Swift's are steps to stamp out something that never should of existed in the first place.

If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of ergonomics, more complex type systems provide power, but require investment in understanding, both conceptually, and in modeling your problem.

You can also adopt automated verification techniques that can prove strong properties about a system automatically.

A comment/correction `io` is stable, its just `chars` directly on a type that implements `Read` that is still unstable, the majority of `std::io` is stable these days.

Its actually much easier then it sounds, we had an undergrad write an entire windowing system on-top of implementing the rest of the OS for undergraduate operating systems at UW in a single quarter (2.5 months~).

I think you guys might find Arrakis interesting: https://arrakis.cs.washington.edu/ it won Best Paper at OSDI '14 and demonstrates a possible way to better use things like virtio.

I think the pain only appears when you start trying to do "deep specification" of large systems. My research group has about 5-10 of us that have all built large systems (5-60 kloc) and verified them in Coq. I know each of us long list of gripes with the tooling.

My recent work has been on a verified JIT compiler and having to write tactics and lemmas to deal with facts about bit vectors seems stupid when SMT solvers are particularly good at this kind of reasoning.

You are correct the current proposed C++ coroutines are vastly different then M:N userspace threading. The allocation differences are drastic, and unlike Go they play nicely with system libraries.

Do you have a compelling use case? I can't imagine a use for untagged unions in Rust that isn't subsumed by other features in the language.

Steve has hit this on the head, there are lots of places where we are using older abstractions that we have had to slowly refactor out of the compiler and like all other software development this won't be instantaneous. We definitely have some less then optimal code in the compiler from a design standpoint.

I think it is also important to recognize that all compilers have this problem and they all stabilize over time. It is an issue orthogonal of safety. These aren't segmentation faults or some kind of memory error but the compiler signaling an internal invariant was violated.

This can happen easily because we are writing a very large program that reads user input, interprets it, and tries to emit a program.

This can happen in multiple situations. One example is the compiler may have a logic bug that violates an internal invariant resulting in an ICE (instead of emitting incorrect code).

Other times it is as simple as the code we have been given is invalid and the error wasn't properly handled, and you end up seeing it in a non-user friendly way (as an ICE).

We are working hard to move the compiler to a more modern, robust design as soon as possible but even with a great design it will be an iterative process that we continue to do over the lifetime of the language, just like everyone else.

Unfortunately safety is not the only concern. Idris' tooling is severely limited. There are very few executables written in Idris (and even fewer that aren't bit-rotted), the build tooling and package management are very simple, the runtime is heavily optimized, concurrent or parallel (like GHC's) and the single-threaded performance is far from Rust's.

I want to be clear that I'm not hating on Idris I love the goals of the project and am probably one of the few people outside the core contributors who has written a backend for the compiler, but you can't really compare a production quality compiler with a full time team of 10 or so to a research compiler worked on by researchers (who have different goals) and volunteers.

Edit: To clarify for this reason I could see why it would be cool to be able to write some critical code in Idris and extract to Rust where you could get performance and tooling for the rest of your application.

Huon is working on SIMD full time at Mozilla this summer as far as I know. We should see more mature support materialize in the next couple of months for sure.

The general the coherence rules stop you from defining an implementation that could be possibly defined elsewhere.

The important take away implications are: - you can not implement a trait defined in another crate for a type defined in another crate, unless the trait is parametrized by a type from the current crate - you can't define overlapping implementations

I'm the author of the above pull request (as well as other pieces of where clauses), unfortunately there are some internals that need refactoring before we can complete equality constraints, and they weren't the highest priority before 1.0 especially since you can encode a trait that acts in the same way. I'm starting at Mozilla for the summer next week and hope to fix a couple of the outstanding issues around them and associated types.

I'm pretty sure even when building a JIT Rust would provide advantages. The only unsafe part of JITing is allocating the underlying instruction buffer and marking the memory as executable to the OS. You could still leverage Rust in building compilers from IR -> Instructions.

Maybe not well understood by programmers but in the programming language world Go's ideas have been around for over 3 decades.

Language choice can be important. If you do the common thing and build a distinct model of your program and prove it correct your guarantees don't hold about the actual implementation. You need a second method to ensure equivalence between your model and implementation, this obviously requires much more work and can vary greatly based on the tools and programming languages involved.

As a current graduate school applicant with a couple of admits to top 10 programs I can confirm this.

My GPA looks "low" around a 3.3 cumulative (I have lots of C's in things I deemed unimportant) but I have a relatively high CS GPA (3.8-3.9), took many graduate classes during undergrad, worked at startups, consulted, did multiple years of research resulting in two publications with 2-3 more in the pipeline, worked on open source, gave talks at workshops and software engineering conferences, TAed, constructed two student led courses, etc.

It seems the most important thing is to demonstrate your ability to work as a researcher (your primary role as a CS graduate student) trumps all in graduate admissions, but that is just my 2 cents.

It seems really strange to compare Coq (a functional language for interactive/automatic theorem proving) to plotting tools.

The core language is almost completely fixed, and the only real changes will be in unstable areas like associated types. There might be some small API changes but all APIs are marked with stability levels so you should be able to figure out what is stable, and what is not.

Researchers will often say things like this about techniques they couldn't get working as a way to explain away their failures. Often times some one will come along a couple years later and do exactly what they claimed was impossible or untenable. I've heard people claim that improvements on their techniques are impossible, and that proposed improvements "won't work" when it in fact does (source: I've seen this happen in the research community more than once).

This may be true about Go, but Rust's traits were very similar to Haskell type classes and now are equivalent in power to Haskell's type classes with several extensions turned on (even though they lack HKTs).

As a side note although clunky HKTs are encodable in Rust and I plan on implementing them natively once we have landed a stable version of 1.0.