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.
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.
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.
> 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.
> 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.
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.
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.
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? :)
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.
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.
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.
> first big push for unit test popularization as being centered on Java and JUnit
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.
I think most people would count java as languages with a less expressive type system. For one it doesn't catch null exceptions, whereas languages like rust do.
> 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.
> 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.
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.
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.
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.
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.
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)
I’m not sure what part of “I get why this shit is useful” is unclear.
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).
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.
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.
> The reason is that it currently still is hard and not worth the effort for >99% of software.
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.
It doesn't sound like you necessarily disagree. Maybe we use different meanings of "worth the effort"?
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.
> The reason why people don't use proofs in software development
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.
> 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.
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.
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.
> 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.
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.
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.
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.
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.
> 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.
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.
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.
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?
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...)
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)
> 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).
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.
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.
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.
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.
+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).
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.
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.
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.
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.
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.
77 comments
[ 3.1 ms ] story [ 160 ms ] threadOn 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.
https://testanything.org
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.
https://github.com/fthomas/refined
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
https://news.ycombinator.com/item?id=38138319
...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.
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.
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.
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.
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
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).
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.
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.
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).
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.