Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Disagree. Effective use of types has a much better cost/benefit than tests, and it's possible to go all the way down to 0% defect rate using just the type system (by encoding proof of correctness into the type system) if you really need to.


I highly doubt that you can prove correctness with types alone.

How would you verify the correctness of this function with types alone:

Integer add(Integer a, Integer b) { return a + b; }

How would types verify for me that the result is correct and not a+b+1?

Formal proofs work for this but to make them work you need more than just types.


The return type of your function is too broad: It should be the "type of integers which can be proven to be the sum of a and b".

That sounds like a joke but it's what going overboard with dependently typed programming languages is like.


Only insofar as your types essentially become the bones of the program... which you'll then want to refactor at some point.

Types are awesome. Languages like Rust give them to me without having to learn a ton of theory. However, eventually, I realise that my types have boxed me into a certain design - and I need to refactor heavily, which involves rewriting a large chunk of my types which I was relying on to show me that my code was correct.


Of course you sometimes need to refactor your types. That's fine; the type checker will guarantee that you can do so safely. You probably want to be cautious about changing your axioms, and to that end it might be worth distinguishing them explicitly, but that's easily done (e.g. you can put them in a separate module).


It'll tell you your program compiles. Unless you've gone seriously overboard and typed every piece of information down to primitives, and built your types so there's no possible way to convert them out of those types at the wrong time, you've still got a chance of having bugs.

Functionality testing will tell you when you've failed to encode an invariant in your type, and there's a good chance that the reason you failed to is just that it's more effort than it's worth. Else we'd all be writing proofs for every program in Coq.


Do your tests also contain every single piece of information?


You can at least add a new test easily when someone reports a bug. Tightening up your types, otoh, is a trade-off against brittleness.

In practice, as I alluded to in my previous post, you really want types combined with broad functionality testing across a range of scenarios. You really don't want to be relying on "it compiles, I assume it works" unless you're able to back out of a deployment in seconds when it doesn't.


Tests are much more brittle than types; automated tooling doesn't know what the tests are saying, and there's no way to make code "test-generic".

Some things are probably not worth typing, but if they're not worth typing they're not worth testing either. Whatever your target defect rate, the most efficient way to hit that target is using types.


> there's no way to make code "test-generic"

Sure there is. Stop testing random bits of internal functionality, start testing huge modules with well-known (semi-public) APIs, or your entire program, and combine that with a ~reasonable~ type system. You want full-system testing. You don't need a whole lot of tests to be sure "it's basically working", and it's a lot easier to turn repeatable bug reports into tests.

When you inevitably break a piece of functionality despite your types, you might not know precisely how it broke, but at least you know it's broken without a customer calling you up. And every time a customer does call you up, you can add a full-functionality test - "this is what the user did, and this is what I expect from that".

Every other engineering branch backs up good practices and solid math with lots of testing. So should we, types or no types.


Been using Scala a lot at work lately and I've definitely helped myself out with using types to good effect, but I still feel like I could be doing better... the one lesson I've definitely learned is if you're going to be serializing things pick a library that makes upgrading those serializations easy or you'll live in fear of changing types.


Yeah, I'd recommend Thrift or Protocol Buffers for serialization. Having distinct serialized objects feels like overhead to start with, but it's well worth it if you ever want to change the code without risking incompatibilities.


What can I read to be convinced of your viewpoint?


I don't know - I reached it through direct experience (a number of years programming professionally in a language with a good type system) rather than anything I read.

https://spin.atomicobject.com/2014/12/09/typed-language-tdd-... makes the case that many tests can be replaced more effectively by types (though the use of Java makes the point less clear than it should be, and means that some properties are so difficult to express through types that the author prefers to use tests). That one can prove correctness with types is well-known, and it stands to reason that there is no need for tests for formally verified code. These two things together suggest that there's never a point on the defect rate/cost curve that's easier to reach with tests than with types, but they don't rule it out entirely.


How would your static typing save you from:

  model.setTitle( dto.getDescription() );


(assuming the bug here is a description being assigned to a title)

getDescription simply needs to return a Description object while getTitle returns a Title object. Duh.

Only in the final rendering should it get turned into a string and there it should only accept a Title type for doing so.

Okay, I'm kind of joking, but this is seriously the solution if you really want to get down to it - primitive overuse is the problem, so wrap it in a type that makes it explicit. You need cheap and easy types to take full advantage of this sort of thing.

EDIT: And even with those reading code developed in such a way may go overboard at some point. I'm not sure as I haven't really seen it done to the fullest extent possible. Typically even when taking a fairly strong advantage of such a type system, unit tests and stuff are still used, but theoretically you could enforce their parameters entirely in the type system. Of course, that enforcement can also be incorrect, but it does make it clearer in many cases.


I can see your argument in some cases, but if you are accepting input, at some point you'll have to accept a string (or any primitive) and convert it to your custom type.

How does static typing ensure you're mapping the correct JSON input fields to your custom types?


> How does static typing ensure you're mapping the correct JSON input fields to your custom types?

Ideally you push it all the way out. Rather than JSON you use Thrift or similar where the messages are strongly typed.

But if you do use JSON, how much benefit does unit testing your JSON mapping really give you? The mapping in code is just a list of field:field pairs, the test is just the same thing, is there really any value in repeating it twice? I'd sooner rely on careful code review than a test.




Consider applying for YC's Winter 2026 batch! Applications are open till Nov 10

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: