Compiling Rust is testing
kobzol.github.io
kobzol.github.io
On the flip side, compiling only proves correctness for the code being compiled, and for the properties covered by the type system. For example, you won’t prove with compiling that your database code works correctly (or at all) with the targeted database product.
It’s important to understand that difference, because otherwise you may think that testing and the static analysis performed by a compiler are interchangeable. They are not.
I agree with you, but I think this is the issue. A lot of people used to working in dynamic languages spend time writing up lots of tests for things that get covered “automatically” in statically typed languages, leading to the confusion you note. This, I’d argue, effects people who “convert” to liking the static language, and to those who think static lands cause only overhead.
This is mostly down to poor testing culture in general. People end up writing a lot of meaningless unit tests when what you need is integration tests. However, there's very little tooling to help with integration tests (in all languages) as everything is focused on unit testing only.
With proper integration tests you will cover much of what the compiler gives you in statically-typed languages.
As an example the approach of 'type correctness through a type checker' and 'type-correctness through integration testing' is largely interchangeable in python. Even though they function very differently.
For normal code bases, this overlap is relatively small (do not need to validate input types, don't need to automatically convert strings to numbers, convert single items to lists, etc), but as you take advantage of the type system, the overlap can become slightly larger (wrap your types, create separate types for validated values, make impossible states impossible).
Granted, no matter how much of a genius you are with the type system, there will always be place for testing, I hope everybody understands that.
I've seen people build type-level DSLs. Sure they encode a lot of logic in types... but are you sure that logic is correct? :)
Java is obviously a statically typed, compiled language with memory safety. But back then everyone still understood the advantages of automated testing. Static typing frees you from a certain class of problems, but it's so far from the whole story, I can't believe it even needs to be said.
Java's type system at the time you're referring to was extremely limited compared to Rust's ML-like type system or even TypeScript. It didn't need to be said back then that the type system wouldn't catch everything because Java's couldn't even catch null pointer exceptions, much less encode error states as algebraic data types or provide zero-overhead newtypes.
I agree that types can't catch everything, but a modern type system like Rust's can be used to prevent many more classes of bugs than just "oops, that was supposed to be an int not a float", and that's all OP is saying: if you're using your type system to its fullest you need many fewer tests than you do in a dynamic language.
Put another way, I feel more confident about my Rust code being correct after it finishes compiling than I do about my Java code when it finishes compiling. And I also feel more confident about my Java code being correct after it finishes compiling than I do about my Python code after... I save the file.
The compiler isn't going to be able to tell you that your fibonacci function actually outputs a sequence of fibonacci numbers. You still have to write tests to prove that just as much in Rust as you do in Java as you do in Python. The fact that Java/JUnit really pushed unit testing hard for the first time is likely just due to the sheer number of Java developers in the enterprise world at the time, and that Java was the big up-and-coming language ecosystem with a lot of money and support and mindshare behind it.
Perl's and TAP came before the xUnit family. TAP quickly spread to many other languages because although we were testing in them, the idea of a standard test engine was new.
Compiling does not prove correctness for any program inputs.
Folks could list (1) compilation errors, and (2) test errors/failures in junit XML or W3C EARL. But typically if code fails to compile, the "test suite" isn't run.
Type checking is not property testing is not fuzzing.
It can.
For example in Scala there are libraries that allow you to define types for inputs e.g. this Int must be non-negative or this String must be greater than 5 characters.
But obviously only for values that are determined within the code.
IIUC e.g. NASA's guidelines specify hard preconditions at the top of every function.
> Hypothesis generates tests from type annotations; and icontract and pycontracts do runtime type checking.
Pynguin also generates tests; but it does not use icontract-style type and value constraints as decorator preconditions in generating tests.
icontract-hypothesis: https://github.com/mristin/icontract-hypothesis
# pseudocode
def main():
a, b = argv[:]
print(add(a, b))
def add(a, b):
return a * b...should a DBA really SSH into the machine and run arbitrary schema changes willy-nilly?
In my ideal workflow, the database admin should write a migration script, open a PR, get it reviewed and merged, released to a staging environment via CI/CD, and when nothing blows up, a CI/CD process should run the schema changes on production.
At any point, you can track down how your database schema looks like, and nowhere in the process I need to worry about the unfortunate case of "oh, yeah, that table, yeah that table looks completely different because Tom was firefighting yesterday night, we have no idea what he did or when, but hopefully we didn't lose any data".
In the environment that I described, sqlx fits in perfectly
(and the DBA would probably get a good talking to for goofing around on live systems in ways that leaves the whole team in the dark, but that's a different issue)
The original comment made a statement about the guarantees static typing and the limitations of those guarantees, the response while making some tangentially valid points called it a “funny example” as if it ran counter to those limitations. But it doesn’t, that’s all.
In this example you are still doing the same compile time verification at runtime. It’s useful, but it’s not making the same type of guarantee.
“ should a DBA really SSH into the machine and run arbitrary schema changes willy-nilly”
Such a straw man. No matter what the process is, mistakes happen, organizational communication breaks down, environment variables don’t get set, there are thousands of reasons your database schema won’t be as expected that have nothing to do with a rogue DBA.
Who said the DBA in my example was acting willy-nilly? Maybe they are following the process. That doesn’t make the static compiled artifacts just disappear. You can put all kinds of additional guards in. These are mostly outside the type system.
Do you believe in your process so thoroughly that you would disable any runtime type checking in sqlx if it had the option? (it doesn’t, for what I thought should be obvious reasons).
A thing which has repeatedly caused apparently competent people to just give up on proving software is Rice's Theorem, sometimes just encountered in the form of "Oh dear, I just realised I'm trying to solve the Halting Problem" (Henry Rice got his PhD for proving that it's not a coincidence, proving any non-trivial semantic requirements of arbitrary programs is always Undecidable)
But Rice's Theorem only means we cannot always be sure. So the important insight is that we're engineers - we mostly want simple, robust, reusable components with easy to prove properties so we often do not care about the edge cases, we can just reject all the programs we can't prove.
That's the crucial technical difference between Rust and C++, but it could have been and in my opinion should be exploited more extensively across the industry.
The reason why people don't use proofs in software development isn't (at least in my experience) because they're delusional about whether that's possible, or even delusional about how hard it is to do in practice. The reason is that it currently still is hard and not worth the effort for >99% of software.
In terms of "complete proof of correctness", you first have to know exactly what you want the software to do. Even completely specifying what you want your software to do in all edge cases isn't worth the effort for most software, let alone implementing it, let alone proving correctness. You don't just "reject" software with edge cases, that's almost all software.
Even if you're looking at proving less ambitious properties than semantic correctness (e.g. memory safety), you can see how much pushback there is against something like Rust. People deny that memory safety is important, complain that the price to pay is too high, complain that the goal isn't really 100% achieved, complain that it compromises something else (performance, simplicity, interoperability, backward-compatibility) to even the slightest degree...
So yes, I agree that formal proofs for software have a role to play and that role will likely increase (although it may not if most software ir replaced by trained black boxes). However, it's not straightforward to say it's "underutilized", and even if it is, it's not due to people reading too much into the halting problem.
That sure sounds like they're delusional to me. Take the vulnerability of smartphones to various vulnerabilities in image codecs over the past few years. That's a solved problem, that's what WUFFS is for, and yet of course Apple doesn't use WUFFS-the-language, or even WUFFS-the-library, they're content that if they can just fix all the bugs in their C++ it'll be fine†. Even Google, which is paying the main author of WUFFS, doesn't use most of it, because hey, they've got handrolled (read, probably riddled with security holes) C++ code... they use his GIF implementation, they might adopt more later, but they haven't yet.
All WUFFS is doing is saying "Oh, if we run a proof checker during compilation we can solve this narrow problem completely" and yet that's apparently too hard. We're not talking about teaching your programmers Coq here or implementing the Principia in Haskell, but what we see over and over is that people would rather cobble together crap that compiles but is garbage and then go home for the day.
† To be fair to Apple their medium/long term plan is to Rewrite It In Swift, but while that's an improvement it is not a guarantee of safety, it's a half measure in some unknowable future.
I meant it in terms of money that a company can save or make from deciding to expend that effort. You also have an additional cost in terms of "risk" that the effort does not yield desired results. So "they're delusional" would only be true if the people deciding this seriously overestimate the effort to verify something or seriously underestimate the benefits. Do you think that's true in general? Or even in the examples you cite?
It seems like Apple and Google know what WUFFS is and what it can and cannot do, so they understand the effort. The maximum conceivable benefits in the cases you mention would be "no security vulnerabilities in said code". I'm not sure that is seen as a huge benefit by those in charge. Even rewriting that stuff in Rust (or even Swift) would significantly reduce the probability of weaknesses being exploited. Nobody seems to think that's worth the effort.
The "marketing pitch" of WUFFS is: "as safe as Go or Rust, roughly speaking, but as fast as C, and that can be used anywhere C libraries are used". So, presumably, Rust and Go are equally and sufficiently safe, "roughly speaking"? And Rust is neither fast enough nor easy enough to integrate with C code (despite being good enough for drives in the Linux kernel)? This sales pitch makes it clear that the people behind WUFFS are keenly aware that "safety" alone doesn't sell.
This problem is generally more endemic of software security in general. The cost of security issues is usually not borne by the people who decide how much to invest into security. Also, security does not contribute to profits, it is only a cost center. By contrast, when you have really important code and you bear the cost of mistakes and outages directly, formal methods are being used where it can be done straightforwardly. AWS and some cryptocurrencies (for whom security and correctness is an above-average part of their sales pitch) have prominent uses.
Static types are proofs, and their use is quite widespread. Of course they are "lightweight" proofs driven by program syntax and targeting very general properties, but they're proofs nonetheless. Any claim that "proofs are not used in software dev" has to be heavily qualified to avoid shifting the goalposts.
Not even close. Compiling cannot even check if your program computes 2+2 correctly, much less anything more complicated (e.g. calculating tax values for a service provided based on, you guessed it, runtime lookups because taxes can and will change).
Compiling with static typing will indeed check that your functions are called with correct input values (for some value of correct) across your codebase.
As an example, there are infinitely many maps from u32 -> u32. But only one map from Minutes -> Seconds. If you use u32 for your times, you need to rely on tests for confidence you have the right math. But if you use Minutes and Seconds, you can rely on the compiler to prove correctness.
Edit: you did say canonical and not unique so I’m probably just being pedantic.
I see where you're coming from, but I think this is only superficially appealing, there's no meat to it. The obvious u32 -> u32 map is identity, in the same way Minutes -> Seconds is a multiplication by sixty, but it's actually not hard to imagine other mappings for the Minutes -> Seconds either, how about given how many Minutes I've been roasting the turkey, how many Seconds should it be rested before carving?
In reality what Rust did here was to offer a Duration type and an Instant type, representing the idea of a period of time (a duration) or a specific moment in time (an instant) and then leverage this idea to have functions like std::thread::sleep take a Duration, so the question of whether we sleep in minutes, second, nanoyears or whatever isn't a question for the sleep function.
Edited to add: These are also important because they're Vocabulary types. By being provided in the standard library (Duration is actually even in core, so it's available on your embedded Rust) these types encourage everybody to agree on vocabulary and enrich the entire ecosystem. Instead of Jim Bob's library working in microseconds and Sarah's library using milliseconds, meaning I must convert everywhere and if I get it wrong it causes chaos, they just both use Durations and everything just works.
Actually, time is difficult. Really difficult.
Some minutes on the real world clock do not have 60 seconds.
If I'm deciding to write something in either Rust or Python, and if part of my decision-making is the develop->test process, then I'm not only going to be thinking about how long it takes to run the test suite after I make a change, but also how much test code and how many tests I'll have to write overall to be satisfied that my code is correct.
Certainly I'll be writing fewer tests in Rust than I will be in Python. Those fewer tests will take less time to run (both because there are fewer of them, and because Python code will run slower than Rust code, on average). And the reason I'll be writing fewer tests is because of Rust's compiler. There are things I will not bother to test all all in Rust, because I will know they are correct when the compiler finishes compiling. But I will have to write tests for those things in Python.
And that's the important point to me: if I can leave out a test in Rust that I'd have to write in Pyhton, and the reason is that Rust's compiler makes the test redundant, then yes, the compiler is actually running tests for me, even if not in the literal sense.
But yes, your main point is what I clicked on the comments to make. Even in testing word-salad-land, compiling is not testing. Neither is using static types. Or foisting the software it on unsuspecting users.
For a lot of languages, yes. For rust, no.
Bought a new computer, tried to compile Mesa, failed: rust compiler too old. Try to compile a newer rust compiler, failed with missing (cargo) dependencies.
So for rust, compiling _is_ testing.
It's also unfortunate the author describes features of static typing as "unit tests" when there's already confusion over the term. I think it works as an analogy, but I think this is a place where not being clear it's an analogy invites confusion.
And yes, I read the article, I know that they literally work on the Rust compiler.
I think the article makes an excellent point. But it begs the question:
Are there compiler flags to disable the 'tests'? If not, it would sure be nice to have them to get the fastest 'make a change -> run test' loop. It would be the best of both worlds. (Unless the developer forgets to run the tests once in a while...)
And as much as people like to talk about rust compile times, it's now actually very fast at compiling small incremental changes in debug mode. The bigger pains are when you are building in release mode, or when you are building from scratch (e.g. first build, updated compiler, updated all your libraries, etc)
This breaks down quickly at scale. If you reach significant code complexity, even with dedicated build machines, remote Bazel builds & distributed caching you're going to wait a long time for single-line changes in a debug `cargo check`. There are some patterns that play well with incremental compilation, but they're easy to break in practice.
I predict as more devs are moving from writing Rust as a hobby (or with focus on smaller libraries) towards larger production systems, we'll see an uptick of frustration with build times. But I'm happy that Rust leadership is aware of the issue (e.g. it was listed as one of the main points in the most recent survey, which made me immensely happy).
Facts on recent developments towards improving Rust's infamous compilation speed issues.
Then we reach the meat of it.
Actually the only compilation time that actually affects development is the time between invoking a test run and the first test running. And...wait for it...it's zero! compilation is testing. Isn't that glorious?
Idk, man.
GO: fast compile, typed, fast testing, pedantic error handling (and I have come to see this as a feature).
I have dabbled in rust. I would much prefer to call out to Rust than C from GO... The fact that this is possible but doesn't feel production ready is something that the rust community can fix. The fact that its complier is holding it back is something that rust needs to fix.
Calling "Compiling Rust Testing" is a hefty dose of copium.
So it's important to benchmark compiles with errors, and make sure those are fast.
One-minute incremental release compiles seem typical. There have been some problems with the optimizer in the linker taking huge amounts of memory if you turn on all the optimizations. A 32GB or larger machine may be needed for some programs.
This is less true when using LSP.
Had no issues with borrow checker or async checks.
It is not "testing", nor it is a substitute for testing but it does play a similar role in discovering and preventing errors.
For me 99.9% of all bugs are detected at compile time.
Whereas when I go back to using Python it's more like 50%.
The overwhelming majority of bugs in software are behavioural bugs, which typing does not catch.
If you want to go down the formalism route to catch bugs then at the bare minimum you require Z formal specifications for all your code.
Do you have Z formal specifications for all your code?
Weak vs. strong typing is orthogonal to static vs. dynamic.
E.g. JS is weak dynamic. Python is strong dynamic. C/C++ are weak static. Haskell, Rust are strong static.
Etc.
And the weak/strong is not binary, it's a spectrum
I find if my typing is really accurate, I introduce fewer bugs! /s
When commiting code you want to make sure it's actually buildable and you didn't accidently type a character somewhere causing it to fail to build. To ensure the codebase is always buildable simply compiling the program is a test that can be done. Checking the validity of code that is utilizing safe abstractions is not something I consider testing.
The Virgil compiler includes an interpreter for the entire language (by necessity--initialization of components can use the full language). This can be exploited to run all of your unit tests in interpreted mode, skipping the compilation step. This is a huge win. It's a win to the point that developing the compiler itself, I often run the compiler in the stable compiler's interpreter (~85ms), to skip the entire bootstrapping step (~400ms).
Why does it always fails with some dependencies issues ?
If rust is so good, why does an old rust compiler (1.58) cannot compile a new rust (1.70) compiler ?
The Rust compiler is not built using stable Rust, and so has very specific requirements for building itself.