Hacker News Reader

Comment by layer8 | Hacker News Reader

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.

View on HN

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.

I don't think it makes sense to expect integration tests have 100% coverage, which is what you would need.

Nothing is really 100% coverage :)

Unless you are sqlite, they might actually credibly have 100% coverage.

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.

https://testanything.org

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.

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.

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.

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

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).

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.

> But only one map from Minutes -> Seconds.

Actually, time is difficult. Really difficult.

Some minutes on the real world clock do not have 60 seconds.

> 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.

https://github.com/fthomas/refined

Are those (non-Enum) precondition value constraints checked at compile-time or at runtime?

Compile time.

But obviously only for values that are determined within the code.

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.

FWIW, in Python, from 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://news.ycombinator.com/item?id=38138319

No it doesn't. How would compiling prove this is wrong?

  # pseudocode
  def main():  
      a, b = argv[:]  
      print(add(a, b))

  def add(a, b):  
      return a * b

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.

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.

Fair point. I meant proofs about semantics, unless stated otherwise. So using tools like HOL and Coq. Can't edit the original comment anymore.

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.

> 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.

> 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.

They specifically said "compiling only proves correctness for the code being compiled, and for the properties covered by the type system".

Reply on news.ycombinator.com