Rust: Beyond the Typechecker
blog.merigoux.ovh
blog.merigoux.ovh
The Stanford Pascal Verifier was probably the first[1] The Pascal-F Verifier, a project I headed around 1980,[2][3] used preconditions and postconditions very similar to what this guy is doing in Rust. "Specifically, full functional correctness with properties like arithmetic correctness, in-bounds array accesses, state machines correctness, functional correctness with respect to an abstract specification or security properties." - we had all that in 1983. Look at the example starting at page 56 in [2].
DEC did a lot of work on this for Modula, and later Java, in the late 1980s.[4] Modula went down with DEC. The work was mostly lost. Dafny is probably the most modern system in this line.
Memory safety by proof was coming along well in the early 1980s. Working systems existed. Automatic prover technology was working. Then came C.
The "array is a pointer" mindset of C set programming back by decades. In Pascal, there were no buffer overflows. Pascal, Modula, Ada, and on to Rust - no buffer overflows. Everything carried along size information. Subscript checking optimizations had been figured out by the 1980s, so the performance penalty was coming down.
The author mentions Sapiens, an attempt to apply machine learning to the problem of null pointers in C. (Anyone have a reference? It's hard to find.) Massive amounts of effort are being applied to try to infer information that C just can't express. This would be a lot more worthwhile if it resulted in translation of C to something better.
Forty years, and this still isn't fixed.
[1] http://i.stanford.edu/pub/cstr/reports/cs/tr/79/731/CS-TR-79... [2] http://www.animats.com/papers/verifier/verifiermanual.pdf [3] https://github.com/John-Nagle/pasv [4] https://link.springer.com/content/pdf/10.1007/BFb0026441.pdf
I agree that software is terrible, and programming language choice plays a big role in what sorts of mistakes you can make, but I'm skeptical that attempting to write provably correct programs is a remotely realistic goal. Sure, it's possible to prove an algorithm, but the real world software systems that need the help--certainly anything that involves more than one process on a single CPU--have complexity that goes well beyond what can be modeled or reasoned about, much less be proven.
Unless the code is in C. Then it's really hard.
[1] https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA...
http://www.ganssle.com/tem/tem372.html#article4
The tools can also miss things. They miss more as complexity goes up. High-assurance systems used to structure things in a hierarchical way with simple functions and only call downs to aid the analysis. Basically, reduce combinatorial explosion. Most software isn't structured anything like that. It does combinatorial explosion with C not giving analyzer a lot of information to begin with. So, it causes tools to miss things.
Rust might be easier to analyze due to the type system. Those labels become inputs and heuristics for future static analyzers.
The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic.
Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.
So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.
And a perfect static analyser with no false negative or false positive is equivalent to solving the halting problem. So what we need is a «good enough» solution working with existing code. But the amount of CVEs and the low adoption of such tools empirically shows that we are far from there.
But usually when it's time to just churn out yet another app, cost-benefit analysis indicates that fuck that, let's use pokemon error handling.
And it's hard to blame anyone for such a decision when the alternative is going a few more days without the shiny new app/feature. The end of the financial quarter is coming. The app/feature must "work".
And that's why it's not surprising that no one uses Coq and Idris for run of the mill business as usual apps.
What I wanted to communicate is that I find that in many cases error handling is a sort of twilight zone. When the environment or context of the running program is not what it should be. (Eg file not found, lack of permission to write to it, not enough memory, something is not configured, missing runtime dependency; and all the state validation errors, etc.) And the errors that result from this are usually too low level, and there is rarely enough information in the error messages (types) themselves to help understand (and potentially work around) the condition causing the error.
Clojure's spec [3] is also promising for better specifications and more automated testing
Over the past decade or so, we have seen many mainstream programming languages adopt functional programming features. My hope is that more mainstream languages adopt preconditions, postconditions, invariants, and useful formal verification features. There are so many more great tools that could be used to build high quality software than unit testing.
[2] https://en.wikipedia.org/wiki/SPARK_(programming_language)
https://github.com/rust-lang-nursery/wg-verification/issues/...
It's good to see that Rust is learning from Ada. Ada is also learning from Rust: https://arxiv.org/abs/1710.07047
K&R was published in 1978. So at best this story and timeline are incomplete.
More illuminating would be an account of why C beat these other languages in the marketplace in the 80s, despite its disadvantages in safety.
Had Bell Labs been allowed to sell UNIX at the same price as other companies were selling theirs, and C would never have taken off.
Burroughs, developed in 1961 in a memory safe systems programming language is still sold by Unisys as ClearPath MCP.
Same applies to the IBM mainframes.
The surviving systems from the 60-70's where C only plays a guest role at most.
The whole point is that contrary to its sales prospect, not only does C also require to write Assembly, it doesn't have any language support for modern hardware CPU/GPUs, just like any other high level language, requiring extensions to the standard, not necessarly portable across implementations.
Check language support across Small-C, Turbo C, Quick C, Aztech C, Metrowerks C and many others from those days.
Likewise it was possible to do the same across Pascal compilers that implemented variants of ISO Extended Pascal/UCSD Pascal, Modula-2 and a couple of other high level languages.
well, we're in 2019 and replacing a few critical .at() by [] regularly allows me to gain a few % when benchmarking.
For this optimization to work, the compiler has to be allowed to report subscript errors early. Frequent subscript checks that cause noticeable overhead tend to be inside loops. Often, the compiler could hoist the implicit assert inside the loop up to one assert checked before the loop is entered. It has to be allowed to report failure as soon as it become inevitable. If you have a loop from 0 to 100 over an array that's 0 to 99, and there's no way to exit the loop early, then failure is inevitable.
As soon as failure is inevitable, it has to be OK to detect it. That means if you're printing values 0 to 100, you'll never even get the first one printed. You'll abort before entering the loop. This is a bit strange to C/C++ programmers.
Once the assert has been hoisted out of the loop, the compiler may be able to prove that it can't fail. For FOR statements, this is usually easy. So the subscript checking overhead can completely disappear for many inner loops.
I have seen plenty of code like that, specially when written by the occasional C++ coder that usually works in other languages.
It's strange but compilers are allowed to do it and anyone sufficiently familiar with undefined behavior will not be surprised.
That's a tricky thing to solve, yeah. At best, under current semantics, the compiler could emit a fast loop and a slow loop, and pick which one using an initial bounds check. But that's extremely awkward at best...
Automatically handling the bounds check upfront is a type of control flow that's halfway between normal exceptions and undefined behavior, that C++ doesn't really grok.
Alternatively, Julia has a macro "@inbounds" which disables checks, but this involves going through and annotating code after testing. You can also start Julia with the options "--check-bounds={yes|no}" to override declarations. Running testsuites enables all checks.
Seems like it would be handy if these checks could be elided by defining a macro. Any reason this isn't done?
The performance cost is often much higher than the time spent repeatedly checking bounds. It tends to defeat the auto-vectorizer.
Another workaround is to manually check bounds before the loop. This lets the compiler prove all bounds checks pass if it gets to the loop, and solves the problem. I do wish that sort of thing could be automatic.
And because of that the tools that do these proofs do not take off, and thus they get reinvented every few years with each programming language.
https://github.com/denismerigoux/rox-star/blob/master/textin...
For instance, the `is_diagonal` function provided as the "correctness checker" looks to me like something that would be in a unit test for the `double` function. However, I think it goes a little bit deeper than that. In a unit test, you are somewhat required to pass specific values to the constructs you are testing. The given example is more complete than a unit test in that it doesn't just test for the correct value being produced by the `double` function when given specific values, it actually checks all possible outcomes by asserting that the `double` function always produces a `Point` where `p.x == p.y`.
Given that the example is relatively trivial, I would like to see how this would work for more complex functions and structures.
Maybe you know this, but this is a well known correspondence (as in academically from decades ago, but barely mentioned in industry): https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.
Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris).
I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
[0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
I wouldn't say using a "unit test" is ever really a viable option for me. Property-based tests subsume unit tests.
So no, Coq and other "total" programing languages (agda, idris, F*) may not be turing complete in the usual sense because the two things are contradictory, but they are much better: you can simulate a turing machine as a server which will be provably always making progress in finite time.
See this paper for some more insights:
https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....
(Contrast with long compile times which are incompressible)
It seems like the philosophy prefers knowing ahead of time what's wrong over discovering it incidentally, and probably accidentally, after the fact.
I discovered a bug that could potentially be triggered in the codebase where I work, but never has. It's about 5 years old.
You don't actually always need technically correct - sometimes you want practically correct, where "practically" covers a huge spectrum.
Because if say, 75% of your time is spent debugging in an "regular" language then you really aren't saving much time by reducing the amount of code you must write.
If we could reduce programming to typing in mostly correct code then software development will be much faster, even if the code we type is 50% longer.
Of course everyone wants the best of both worlds: everything now, zero bugs. Fast, cheap, right: pick two applies despite everyone wanting all three.
I thought we were discussing the trade-offs of typing a little more to guarantee correctness, or at least eliminate a class of software errors.
You're doing that Appeal to the Extremes Fallacy:
https://www.logicallyfallacious.com/tools/lp/Bo/LogicalFalla...
I'm not falling into appeal to extreme, even though I did point out an extreme.
I'll disagree with this one. Refactoring old and rarely-touched code is bliss when working under a strong type system, at least relative to dynamic or weakly-typed languages. The key to the timely resolution of technical debt is to allow things to be updated in piecemeal rather than in one enormous burst; this requires solid abstraction boundaries and encapsulation, both of which are provided by types (in addition to other features of a language, such as a module system). The fact that Rust so heavily discourages global state is another point in its favor.
We can agree that there are contexts where correctness is less important than velocity, e.g. prototyping, though languages that front-load correctness at the expense of velocity are going to produce less technical debt in the first place, because the debts can be paid off before they accrue interest.
That said, it’s not that simple. There are threshold effects (more than X amount of time = your company is dead) and intangibles (how do you feel while programming).
But anyone making a blanket statement without considering these things is participating in a dumb internet argument.
How is this confusing?
If it takes you 2 weeks with language X to write a sloppily written app, that works 99% of the time but has some errors -- and 2 months with Rust to write a version of the same app that has no errors, what you'd you prefer?
Ever heard of "time to market"? What good it would be if you get it 100% right, and your competitor has their app already out, and captured all your potential customers?
And even if time to market is not involved, would you really care for some occasional errors, if you get the majority of the functionality you want working just fine?
If you build pacemakers and airplanes, the answer is yes.
If you build regular websites, apps, and scripts, the answer might very well be no.
That's the case, just the numbers (2 weeks, 100% etc) are made up.
It’s a large, multi-variable problem. This is why it’s great that we have so many languages!
A constant stream of bugs have driven customers away before too, so if you're waiting in the wings with a bug-free/verified version of your competitor's program, you have a real shot at stealing their customers. First mover advantage is important, but so is quality if marketed properly.
I admit personally I'm inclined to agree with coldtea. But one example where I think the stability/quality of the software really did play an important role is WhatsApp. I remember when there were a bunch of competing services, but WhatsApp was the only reliable one. As far as I can tell there was nothing else that WhatsApp did better, and yet they 'won' (at least in Holland/Europe).
Microsoft had a features-first mindset, which led to a Swiss-cheese-manifold of bugs and security flaws.
The result was that you couldn't install anything without risking a virus.
Businesses went with browser based solutions to avoid that risk.
The interesting part is, WhatsApp is built using a dynamically-typed language whose guiding principle is to "let it crash." Your code will have bugs so plan accordingly.
if it takes 2x or 3x to get to the next iteration then what’s the point... (again, assuming we aren’t talking pacemakers etc)
just my feeling, but these low level languages that try to have it both ways (working in the bit/byte realms, but also super high correctness) aren’t suitable for the realm of high iteration.... instead some high level language amenable to rapid iteration but still have high reliability should instead be built on top of something like rust but not necessarily _in_ it...
[edit] forgot to mention parent post
But this is a classic race to the bottom, and regulation is coming. The days when you could write an app that takes a person's information and stores it negligently are drawing to a close. Given sufficient liability penalties, the economic question will shift away from "what if we're late" to "what if it's broken", and that's when you'll start seeing a shift away from languages like C/C++ (and probably also languages like Python and JavaScript) towards languages/platforms/tooling that provide strong, indemnifying guarantees.
Like BS regulations in cheese, wine making etc, has eliminated small regional producers (once dominant) in favor of large conglomerates -- at least France is somewhat holding up.
- Exempt smaller organizations. Maybe the classic example is the ACA in the US; if you're under a certain number of employees you don't need to provide health care. Obvious pitfalls, but still an option.
- Provide subsidies. This isn't exactly going to let a 10 person shop compete with someone like Airbus, but it does let you do things like hire staff and purchase tools to comply with regulations.
And separate from all that, it would be cool if we started enforcing antitrust legislation in the US again.
I have the assumption that once I am fluent in rust, more and more of the first code I write will be accepted by the borrow checker. The analogy is to C, where I don't really have to think consciously about, for example, assigning and dereferencing pointers. When I was a beginner C programmer (many years ago), I would write code and have it SIGSEGV immediately during test. Now that just doesn't happen unless I'm getting WAY too clever.
I have heard more than once that if we could spend a few hours less developing at the cost of having the product need to reboot every day or so, it was worth it. Of course it was no safety critical code, but in the end the only discriminant is money.
That software's users will use the product is the number one metric. They'll use it so long as it achieves their goal with the reliability or security they tolerate. That often means it can be kind of flaky in terms of reliability. The security can be arbitrarily bad so long as they don't know it. Sometimes they'll still use the product if they know security is bad because they need it.
That's the baseline. From there, developers have to decide what's most beneficial among investments in more features, enhancements of existing features, new products/activities, or enhancing quality/reliability/security. They usually choose against that last set. So, doing the other things with the minimum quality that's acceptable makes the most economic and social sense.
Although I must say that it replaced Python for most more complex programs for me. The type system makes it easier to read somebody elses code, even if they skipped all documentation.
Rust certainly forces good practice onto you. But on bigger projects good practice doesn’t reduce your productivity, but instead increases it, let alone to speak of the increased sustainability. Rust’s module system in combination with it’s type system and ownership rules leave very little dark spots for the programmer where weird things can happen, even when your project grows big. And if weird things happen they are a breeze to track down compared to python, usually. Rust sort of nudges you into the right choices, when you program Rust the Rust way.
If you are constantly fighting with the type system and the borrow checker that means you are probably still clinging to concepts you brought from other languages (at least it was like this for me). The moment I said: “Ok Rust, you won, from now on I will do it your way”, was the moment the compiler got my friend and things start to flow. Looking back I wonder why I ever thought I have to be able to force my abstractions into the code instead of taking a more data centric approach.
Is the productivity significantly lower than with python? Only if you are not firm with the language
I really hope this will be the next mainstream thing in programming language design, after the current functional wave. Even without fully perfected static analysis tools, just the dynamic checks alone are well worth the trouble of writing good contracts, IMO. They also make for better, more precise documentation.
The foundational ideas around DbC and Eiffel for requirements and their proof still evolve and progress 33 years later with AutoReq. A paper describing AutoReq was recently published ..
AutoReq: Expressing and verifying requirements for control systems https://www.sciencedirect.com/science/article/pii/S1045926X1...
I recall someone mentioning in a RFC that it was on a distant wishful thinking roadmap. I hope it is.
1: https://github.com/rust-lang/rfcs/issues/1930
2: https://github.com/rust-lang/rfcs/pull/1657#issuecomment-268... and https://github.com/rust-lang/rfcs/pull/1931#issuecomment-304...
3: https://github.com/rust-lang/rfcs/blob/master/text/2000-cons...
We may or may not end up with them someday, but we need experience with RFC 2000 first.
fn foo<T>(array: [T; ?]) {
When the RFC I referenced above is implemented, you’d write
fn foo<T, const N>(array: [T; N]) {
(In today’s Rust you’d use a slice instead, but that’s the simplest example I can give.)
While I was at NASA I was advocating for using Rust instead of C/C++ and FORTRAN and many people were interested because of the safety/performance aspects. I think it would take some serious ground from them in that area with dependent types also.
The nice thing about this kind of static analysis for critical systems is that there are often extreme consequences if a runtime check fails. What do we do for the nuclear power control system when we detect an error? Crash? Shut down the system? But the system is not functioning properly. How do we know that we can safely shut it down? These are pretty horrible things to consider. It's much better to be able to say analytically that the situation can not happen.
I once worked in a high energy physics lab, though. There is always memory corruption to contend with, so you'll never be free of runtime errors ;-)
The formal verification method used by SPARK is industry-proven (for decades). Dependent types are for the most part still an academic curiosity struggling to find industrial application. Of course they may very well do that, one day. But today, if you're working on safety-critical systems, I hope you take a close look at Ada+SPARK.
But actually i must say i'm not very fond of these kind of approaches. As is rightly made explicit in the post, a lot of nice properties of Rust come from it's type system. A type system is a way to annotate usual programming constructs with additional infos (types) together with a decidable procedure for testing whether or not a particular program is well-typed. And then we provide several key lemmas asserting that all well-typed program enjoy such and such property. On the other hand, program verification is a different beast: you annotate parts of your program with some form of specification (hoare triplets and the like) and then you try to solve the (in most case undecidable) problem of coming up with proofs that your program satisfies the specifications you gave.
The approach is very different: on one hand you restrict (maybe severely) the programs so that you can decide whether or not some properties hold, on the other hand you (mostly) don't restrict the programs and you hope to give enough hints so that the solver doesn't get stuck. Bottom-up versus top-down. Correct-by-construction versus maybe-provably-correct. I feel like type checking is robust/reliable/simple whereas verification is a black-box which isn't easy to understand and thus never feels very "principled". Sure types can sometimes be too explicit and heavy on the user, but they are also more predictable and consistent.
My 2cts... Anyway i'm not saying i think this project is useless or anything, most systems actually live somewhere between bottom-up and top-down, ideas from one side may help the other, and deductive verification may arguably be much more bottom-up than other verification techniques (all flavors of model checking, abstract interpretation etc).
It is still unclear how best to use such code level verification, as the effort required grows very quickly with code size, and it's unclear how much sporadic verification of properties that are easy to prove actually improves correctness, but this is all still ongoing research.
Refinement types are also worth exploring in this space, as they appear to give a good power-to-weight. See Liquid Haskell, for example, https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-bas...
https://blog.rust-lang.org/2019/04/11/Rust-1.34.0.html#custo...
From tooling perspective, this isn't perfect, because there's still no guarantee that the token stream is a valid expression. So e.g. an IDE trying to highlight them or do a global rename refactor has to assume, which might not always be correct for token-based DSLs. It would be nice to have some metadata to distinguish those. Or perhaps there is an idiomatic way to express it in a contract on the macro itself, that tools could look at?
They call it "design by contract" rather than "deductive verification" though.
Wish there wouldn't be so many terms for the same thing.
edit: There's also an existing RFC for this: https://github.com/rust-lang/rfcs/issues/1077
The same with the RFC, it dismissed automatic verification: "Automated proof systems are very hard, especially when AFAIK Rust's type system doesn't even have partial formal proofs yet."
This paper shows a similar approach to OP's but applied to Curry: https://arxiv.org/abs/1709.04816. It shows how no formal proofs are needed. However Curry is significantly more pure.
Why doesn’t this category of bugs exist for Rust programs? Simply
because you cannot write a program that contains a null-pointer error.
$ nl -ba nulltmp.rs
1 use std::ptr;
2
3 fn main() {
4 unsafe {
5 let p = ptr::null::<i64>();
6 println!("{}", *p);
7 }
8 }
$ rustc nulltmp.rs
$ ./nulltmp
Segmentation fault (core dumped)
"I do not intend to tackle the difficult problem of interaction between unsafe and safe Rust code; Rustbelt is the correct way to do it."
The statement you quoted is clearly in the implied context of safe code.
Clearly you don't.