8 ms·

Compiling Rust is testing

62 points by ingve 3y ago

layer8 3y ago
No, compiling is proving, not testing. This is fundamentally different. Testing can only demonstrate the correctness for the data being tested with (and for the execution paths exercised). Compiling proves correctness properties for all executions and all inputs. Compiling with a static type system is like proving a mathematical theorem. Testing is like evaluating a mathematical formula for specific inputs. 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.
- a_humean 3y ago
  I think the point in the article is coming from Python or languages with less expressive type systems there is an awful lot of overlap between compiling/type checking in rust and some of the tests that get written in those languages.
  - layer8 3y ago
    It’s fundamentally different. Testing in a dynamic language will never ensure that your variable always holds a string and never a number. Compiling a statically-typed language however does exactly that. This difference is the same for all checks a compiler performs. 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.
    - FridgeSeal 3y ago
      > 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.
      - troupo 3y ago
        > spend time writing up lots of tests for things that get covered “automatically” in statically typed languages 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.
        thunky 3y ago
        I don't think it makes sense to expect integration tests have 100% coverage, which is what you would need.
        troupo 3y ago
        Nothing is really 100% coverage :)
        a_humean 3y ago
        Unless you are sqlite, they might actually credibly have 100% coverage.
    - rocqua 3y ago
      Testing and analysis aren't equivalent, but they can be similar enough in use to be interchangeable. 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.
    - serial_dev 3y ago
      They are not interchangeable but there is an overlap. 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.
      - troupo 3y ago
        And if your type system is expressive ... you might still need to write tests to make sure that your types are correct and give you back the result you actually want :) 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? :)
  - TillE 3y ago
    I've seen that take a lot lately, and it's odd because I remember the first big push for unit test popularization as being centered on Java and JUnit. 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.
    - lolinder 3y ago
      If when you hear "there's a lot of overlap between type checking and unit testing" your first thought is of Java's type system then I can definitely see why you'd be concerned. 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.
    - kelnos 3y ago
      Java's type system is pretty limited when compared to Rust's, and Rust as a language is designed to eliminate certain classes of bugs, some of which can still happen in a successfully-compiled Java program. Certainly javac can help you prove correctness in some cases, but rustc can prove that in many more. (Also consider that, during the time period you're referring to, Java's type system was even more limited than it is now.) 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.
- westurner 3y ago
  > Compiling proves correctness properties for all executions and all inputs 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.
  - threeseed 3y ago
    > Compiling does not prove correctness for any program inputs. 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. https://github.com/fthomas/refined https://github.com/fthomas/refined
    - westurner 3y ago
      Are those (non-Enum) precondition value constraints checked at compile-time or at runtime?
      - threeseed 3y ago
        Compile time. But obviously only for values that are determined within the code.
        westurner 3y ago
        What does Rust do at runtime if you pass a non-const to a const field at a low level at runtime? If there's no runtime type or and value constraint checking, IMHO it shouldn't be considered proven at all. IIUC e.g. NASA's guidelines specify hard preconditions at the top of every function.
      - westurner 3y ago
        FWIW, in Python, from https://news.ycombinator.com/item?id=38579378 https://news.ycombinator.com/item?id=38579378 : > 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 https://github.com/mristin/icontract-hypothesis https://news.ycombinator.com/item?id=38138319 https://news.ycombinator.com/item?id=38138319
- wongarsu 3y ago
  Databases are a funny example. One of the most popular database libraries in rust is sqlx, which will typecheck your SQL against a running database. Of course it can't prove that your SQL does what you want it to, but it goes very far in ensuring that the database won't outright reject your queries and that types are respected.
  - jeremyloy_wt 3y ago
    Oh is that what the online/offline stuff in their docs mean? I’ve never heard of that technique being used before, that’s really interesting
    - wongarsu 3y ago
      Exactly. Normally it will use whatever database you put in your DATABASE_URL environment variable (or .env), but you can run `cargo sqlx prepare` to save the metadata in a bunch of json files to enable offline development or if you CI environment doesn't have a database instance. However you will need to update this every time you change a SQL query. I find it more convenient to just develop in online mode against a local database.
  - epcoa 3y ago
    Does it also plant a trojan in the DB for the next time the DBA attempts to change the schema? I get why this shit is useful but it really doesn’t respond to the parent comment - you’re still getting runtime checks.
    - serial_dev 3y ago
      I might just be naive, or you and I worked at places where different practices were implemented, but... ...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)
- tialaramex 3y ago
  Indeed, this is extremely powerful and underutilized, even though as you correctly note it's not a replacement for testing in practice. 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.
  - staunton 3y ago
    As someone who really enjoys formal proofs and loves playing with the tools used for it (and seeing the huge progress being made there), I have to strongly disagree with this framing. 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.
- troupo 3y ago
  > Compiling proves correctness properties for all executions and all inputs. Compiling with a static type system is like proving a mathematical theorem. 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.
  - mkarrmann 3y ago
    They specifically said "compiling only proves correctness for the code being compiled, and for the properties covered by the type system".
- phamilton 3y ago
  I really like the idea of canonical maps/morphisms. The idea is that there exists one and only one possible implementation of a given type transformation. For code constructed of canonical morphisms, the compiler can prove correctness. 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.
  - dullcrisp 3y ago
    Couldn’t you lift any of your u32 -> u32 maps to a map from Minutes -> Minutes or Seconds -> Seconds and then compose with your canonical map to get a different Minutes -> Seconds map? Edit: you did say canonical and not unique so I’m probably just being pedantic.
  - tialaramex 3y ago
    > As an example, there are infinitely many maps from u32 -> u32. But only one map from Minutes -> Seconds 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.
  - drewcoo 3y ago
- kelnos 3y ago
  I feel like you're just arguing semantics and strict language use, which is what I think the article is deliberately -- and usefully -- ignoring. 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.
  - diarrhea 3y ago
    A bit tangential, but wanted to point out how modern Python gets surprisingly close (in the pragmatic sense) to Rust in terms of replacing tests with type-level correctness checks (proofs?). I realise you used Python merely as an example. For example, Python can do structural pattern matching with exhaustiveness checking on the type level nowadays. It lacks discriminated unions, the ultimate secret ingredient, so will keep lagging behind in that area sadly.
  - layer8 3y ago
    In my experience it’s mostly orthogonal. I don’t write significantly less tests in statically-typed languages than in dynamically-typed languages. There’s just too many things that depend on the runtime behavior, on having implemented the correct program logic and algorithms (which a compiler can’t check). Statically-typed languages do give me higher confidence in the correctness of the program with regard to the invariants covered by the type system, but they don’t do a lot for the program logic that is being tested.
- drewcoo 3y ago
  Well . . . testing, checking, proving, validation, verification, etc. are awfully closely related terms and people don't agree on definitions for them. And that's just scratching the surface of the "OMG What Is Testing" lexicon! 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.
- hulitu 3y ago
  > No, compiling is proving, not testing. This is fundamentally different. Testing can only demonstrate the correctness for the data being tested with (and for the execution paths exercised). Compiling proves correctness properties for all executions and all inputs. Compiling with a static type system is like proving a mathematical theorem. Testing is like evaluating a mathematical formula for specific inputs. 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.
- chuckhend 3y ago
  Compare this with a language like python -- you'll end up writing a lot of tests which do nothing but assert types of python objects. Compared to rust, the compiler is 'proving' that your code is set up with the right types. Switching from python to Rust, there's tests you don't have to write and you get immediate validation on that class of problems them via the compiler.
charcircuit 3y ago
I disagree with the reasoning, but agree with the conclusion. 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.
refulgentis 3y ago
Strange to read. 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.
deleted 3y ago
[deleted]
hulitu 3y ago
> Compiling Rust Is Testing 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 ?
- deleted 3y ago
  [deleted]
- steveklabnik 3y ago
  > 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.
thesuperbigfrog 3y ago
Strong typing helps to catch more errors at compile time versus weak typing. It is not "testing", nor it is a substitute for testing but it does play a similar role in discovering and preventing errors.
- ReflectedImage 3y ago
  It's only around 1% of errors, it's not very good.
  - threeseed 3y ago
    In Scala we have a robust type system and so it's possible to model out your application through types. 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%.
    - ReflectedImage 3y ago
      Then you are shipping some incredibility buggy software then whether you are aware of that or not. 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?
- troupo 3y ago
  You're confusing typing categories :) 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
  - drewcoo 3y ago
    > You're confusing typing categories :) I find if my typing is really accurate, I introduce fewer bugs! /s
HL33tibCe7 3y ago
This is cope
708733454927516 3y ago
(non-Rust user; dum question warning...) 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...)
- wongarsu 3y ago
  There is the opposite, you can only run correctness checks without compiling by doing `cargo check` (though your IDE is probably already doing that for you). But compiling without these checks isn't really possible, since the later stages of the compiler rely on the assumptions guaranteed by the earlier stages. You can't skip type checks and still know that you're generating valid code. 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)
  - dist1ll 3y ago
    > it's now actually very fast at compiling small incremental changes in debug mode. 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).
actuallyalys 3y ago
It's unfortunate that the author used the word "testing" because I think the underlying point is correct: By the time you've compiled Rust, there's been a significant number of automated checks against your code, which less true of a language like Python. 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.
distortionfield 3y ago
I like rust as much as the next guy but this is just hilarious Rust apologia. Insisting that your long compile times are ackchually tests is comedy gold. And yes, I read the article, I know that they literally work on the Rust compiler.
- munchler 3y ago
  Not only that, but also claiming that Rust is somehow superior to other statically-typed languages in this regard. I think functional programming language like Haskell, F#, etc. deserve more of the credit here.
zer00eyz 3y ago
The fact that he brings up GO, and then doesn't compare it to rust/python is amusing. 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.
titzer 3y ago
+1 to implementing a Rust interpreter. You can skip the entire middle and backend of the compiler, and if the program doesn't do much, this will be faster than any other solution. 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).
FpUser 3y ago
Let's not to play with the words and be a weasel. Building Rust project is slow. Selling slow builds as a testing feature is very misleading at best.
- bfrog 3y ago
  Slow builds are never a joy but.. if you save hours debugging and writing tests for stuff the typesystem and language already check for you, is it worth the trade off in compile time? I found myself saying it was almost every time I used rust for a program myself.
  - FpUser 3y ago
    I work with strongly typed compiled languages (well others as well but that's not the point). If I need change / compile / run iterations slow builds are a big time waster.
_dain_ 3y ago
You don't even have to compile it though ... just set up rust-analyzer to run in your IDE and it will tell you about type errors and ownership fuckups every time you edit the file.
Animats 3y ago
There's an important point here, which somehow got lost in that article. For Rust, it's important that unsuccessful compiles be fast. Development usually involves far more failed compiles than successful ones, as you satisfy all the consistency conditions which Rust enforces. When the program finally compiles, there's a good chance it will work. 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.
- ivanjermakov 3y ago
  > Development usually involves far more failed compiles than successful ones This is less true when using LSP.
  - Animats 3y ago
    LSP just does local syntax. Not cross-module checks, including the borrow checker. The Rust compiler catches local syntax errors very quickly, so that's not a big issue.
    - ivanjermakov 3y ago
      Modern LSP servers are capable of workspace-level diagnostics, from my experience with tsserver and rustanalyzer. Had no issues with borrow checker or async checks.
bfrog 3y ago
I mean the way rust is written, in a way you don’t need to write nearly as many tests I found so.. in a way I believe this to be true.

62 points by ingve 3y ago

No, compiling is proving, not testing. This is fundamentally different. Testing can only demonstrate the correctness for the data being tested with (and for the execution paths exercised). Compiling proves correctness properties for all executions and all inputs. Compiling with a static type system is like proving a mathematical theorem. Testing is like evaluating a mathematical formula for specific inputs. 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.

a_humean 3y ago
I think the point in the article is coming from Python or languages with less expressive type systems there is an awful lot of overlap between compiling/type checking in rust and some of the tests that get written in those languages.
- layer8 3y ago
  It’s fundamentally different. Testing in a dynamic language will never ensure that your variable always holds a string and never a number. Compiling a statically-typed language however does exactly that. This difference is the same for all checks a compiler performs. 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.
  - FridgeSeal 3y ago
    > 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.
    - troupo 3y ago
      > spend time writing up lots of tests for things that get covered “automatically” in statically typed languages 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.
      - thunky 3y ago
        I don't think it makes sense to expect integration tests have 100% coverage, which is what you would need.
        troupo 3y ago
        Nothing is really 100% coverage :)
        a_humean 3y ago
        Unless you are sqlite, they might actually credibly have 100% coverage.
  - rocqua 3y ago
    Testing and analysis aren't equivalent, but they can be similar enough in use to be interchangeable. 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.
  - serial_dev 3y ago
    They are not interchangeable but there is an overlap. 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.
    - troupo 3y ago
      And if your type system is expressive ... you might still need to write tests to make sure that your types are correct and give you back the result you actually want :) 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? :)
- TillE 3y ago
  I've seen that take a lot lately, and it's odd because I remember the first big push for unit test popularization as being centered on Java and JUnit. 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.
  - lolinder 3y ago
    If when you hear "there's a lot of overlap between type checking and unit testing" your first thought is of Java's type system then I can definitely see why you'd be concerned. 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.
  - kelnos 3y ago
    Java's type system is pretty limited when compared to Rust's, and Rust as a language is designed to eliminate certain classes of bugs, some of which can still happen in a successfully-compiled Java program. Certainly javac can help you prove correctness in some cases, but rustc can prove that in many more. (Also consider that, during the time period you're referring to, Java's type system was even more limited than it is now.) 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.
westurner 3y ago
> Compiling proves correctness properties for all executions and all inputs 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.
- threeseed 3y ago
  > Compiling does not prove correctness for any program inputs. 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. https://github.com/fthomas/refined https://github.com/fthomas/refined
  - westurner 3y ago
    Are those (non-Enum) precondition value constraints checked at compile-time or at runtime?
    - threeseed 3y ago
      Compile time. But obviously only for values that are determined within the code.
      - westurner 3y ago
        What does Rust do at runtime if you pass a non-const to a const field at a low level at runtime? If there's no runtime type or and value constraint checking, IMHO it shouldn't be considered proven at all. IIUC e.g. NASA's guidelines specify hard preconditions at the top of every function.
    - westurner 3y ago
      FWIW, in Python, from https://news.ycombinator.com/item?id=38579378 https://news.ycombinator.com/item?id=38579378 : > 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 https://github.com/mristin/icontract-hypothesis https://news.ycombinator.com/item?id=38138319 https://news.ycombinator.com/item?id=38138319
wongarsu 3y ago
Databases are a funny example. One of the most popular database libraries in rust is sqlx, which will typecheck your SQL against a running database. Of course it can't prove that your SQL does what you want it to, but it goes very far in ensuring that the database won't outright reject your queries and that types are respected.
- jeremyloy_wt 3y ago
  Oh is that what the online/offline stuff in their docs mean? I’ve never heard of that technique being used before, that’s really interesting
  - wongarsu 3y ago
    Exactly. Normally it will use whatever database you put in your DATABASE_URL environment variable (or .env), but you can run `cargo sqlx prepare` to save the metadata in a bunch of json files to enable offline development or if you CI environment doesn't have a database instance. However you will need to update this every time you change a SQL query. I find it more convenient to just develop in online mode against a local database.
- epcoa 3y ago
  Does it also plant a trojan in the DB for the next time the DBA attempts to change the schema? I get why this shit is useful but it really doesn’t respond to the parent comment - you’re still getting runtime checks.
  - serial_dev 3y ago
    I might just be naive, or you and I worked at places where different practices were implemented, but... ...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)
tialaramex 3y ago
Indeed, this is extremely powerful and underutilized, even though as you correctly note it's not a replacement for testing in practice. 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.
- staunton 3y ago
  As someone who really enjoys formal proofs and loves playing with the tools used for it (and seeing the huge progress being made there), I have to strongly disagree with this framing. 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.
troupo 3y ago
> Compiling proves correctness properties for all executions and all inputs. Compiling with a static type system is like proving a mathematical theorem. 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.
- mkarrmann 3y ago
  They specifically said "compiling only proves correctness for the code being compiled, and for the properties covered by the type system".
phamilton 3y ago
I really like the idea of canonical maps/morphisms. The idea is that there exists one and only one possible implementation of a given type transformation. For code constructed of canonical morphisms, the compiler can prove correctness. 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.
- dullcrisp 3y ago
  Couldn’t you lift any of your u32 -> u32 maps to a map from Minutes -> Minutes or Seconds -> Seconds and then compose with your canonical map to get a different Minutes -> Seconds map? Edit: you did say canonical and not unique so I’m probably just being pedantic.
- tialaramex 3y ago
  > As an example, there are infinitely many maps from u32 -> u32. But only one map from Minutes -> Seconds 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.
- drewcoo 3y ago
kelnos 3y ago
I feel like you're just arguing semantics and strict language use, which is what I think the article is deliberately -- and usefully -- ignoring. 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.
- diarrhea 3y ago
  A bit tangential, but wanted to point out how modern Python gets surprisingly close (in the pragmatic sense) to Rust in terms of replacing tests with type-level correctness checks (proofs?). I realise you used Python merely as an example. For example, Python can do structural pattern matching with exhaustiveness checking on the type level nowadays. It lacks discriminated unions, the ultimate secret ingredient, so will keep lagging behind in that area sadly.
- layer8 3y ago
  In my experience it’s mostly orthogonal. I don’t write significantly less tests in statically-typed languages than in dynamically-typed languages. There’s just too many things that depend on the runtime behavior, on having implemented the correct program logic and algorithms (which a compiler can’t check). Statically-typed languages do give me higher confidence in the correctness of the program with regard to the invariants covered by the type system, but they don’t do a lot for the program logic that is being tested.
drewcoo 3y ago
Well . . . testing, checking, proving, validation, verification, etc. are awfully closely related terms and people don't agree on definitions for them. And that's just scratching the surface of the "OMG What Is Testing" lexicon! 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.
hulitu 3y ago
> No, compiling is proving, not testing. This is fundamentally different. Testing can only demonstrate the correctness for the data being tested with (and for the execution paths exercised). Compiling proves correctness properties for all executions and all inputs. Compiling with a static type system is like proving a mathematical theorem. Testing is like evaluating a mathematical formula for specific inputs. 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.
chuckhend 3y ago
Compare this with a language like python -- you'll end up writing a lot of tests which do nothing but assert types of python objects. Compared to rust, the compiler is 'proving' that your code is set up with the right types. Switching from python to Rust, there's tests you don't have to write and you get immediate validation on that class of problems them via the compiler.

charcircuit 3y ago

I disagree with the reasoning, but agree with the conclusion. 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.

refulgentis 3y ago

Strange to read. 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.

deleted 3y ago

[deleted]

hulitu 3y ago

> Compiling Rust Is Testing 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 ?

deleted 3y ago
[deleted]
steveklabnik 3y ago
> 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.

thesuperbigfrog 3y ago

Strong typing helps to catch more errors at compile time versus weak typing. It is not "testing", nor it is a substitute for testing but it does play a similar role in discovering and preventing errors.

ReflectedImage 3y ago
It's only around 1% of errors, it's not very good.
- threeseed 3y ago
  In Scala we have a robust type system and so it's possible to model out your application through types. 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%.
  - ReflectedImage 3y ago
    Then you are shipping some incredibility buggy software then whether you are aware of that or not. 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?
troupo 3y ago
You're confusing typing categories :) 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
- drewcoo 3y ago
  > You're confusing typing categories :) I find if my typing is really accurate, I introduce fewer bugs! /s

HL33tibCe7 3y ago

This is cope

708733454927516 3y ago

(non-Rust user; dum question warning...) 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...)

wongarsu 3y ago
There is the opposite, you can only run correctness checks without compiling by doing `cargo check` (though your IDE is probably already doing that for you). But compiling without these checks isn't really possible, since the later stages of the compiler rely on the assumptions guaranteed by the earlier stages. You can't skip type checks and still know that you're generating valid code. 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)
- dist1ll 3y ago
  > it's now actually very fast at compiling small incremental changes in debug mode. 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).

actuallyalys 3y ago

It's unfortunate that the author used the word "testing" because I think the underlying point is correct: By the time you've compiled Rust, there's been a significant number of automated checks against your code, which less true of a language like Python. 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.

distortionfield 3y ago

I like rust as much as the next guy but this is just hilarious Rust apologia. Insisting that your long compile times are ackchually tests is comedy gold. And yes, I read the article, I know that they literally work on the Rust compiler.

munchler 3y ago
Not only that, but also claiming that Rust is somehow superior to other statically-typed languages in this regard. I think functional programming language like Haskell, F#, etc. deserve more of the credit here.

zer00eyz 3y ago

The fact that he brings up GO, and then doesn't compare it to rust/python is amusing. 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.

titzer 3y ago

+1 to implementing a Rust interpreter. You can skip the entire middle and backend of the compiler, and if the program doesn't do much, this will be faster than any other solution. 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).

FpUser 3y ago

Let's not to play with the words and be a weasel. Building Rust project is slow. Selling slow builds as a testing feature is very misleading at best.

bfrog 3y ago
Slow builds are never a joy but.. if you save hours debugging and writing tests for stuff the typesystem and language already check for you, is it worth the trade off in compile time? I found myself saying it was almost every time I used rust for a program myself.
- FpUser 3y ago
  I work with strongly typed compiled languages (well others as well but that's not the point). If I need change / compile / run iterations slow builds are a big time waster.

_dain_ 3y ago

You don't even have to compile it though ... just set up rust-analyzer to run in your IDE and it will tell you about type errors and ownership fuckups every time you edit the file.

Animats 3y ago

There's an important point here, which somehow got lost in that article. For Rust, it's important that unsuccessful compiles be fast. Development usually involves far more failed compiles than successful ones, as you satisfy all the consistency conditions which Rust enforces. When the program finally compiles, there's a good chance it will work. 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.

ivanjermakov 3y ago
> Development usually involves far more failed compiles than successful ones This is less true when using LSP.
- Animats 3y ago
  LSP just does local syntax. Not cross-module checks, including the borrow checker. The Rust compiler catches local syntax errors very quickly, so that's not a big issue.
  - ivanjermakov 3y ago
    Modern LSP servers are capable of workspace-level diagnostics, from my experience with tsserver and rustanalyzer. Had no issues with borrow checker or async checks.

bfrog 3y ago

I mean the way rust is written, in a way you don’t need to write nearly as many tests I found so.. in a way I believe this to be true.