Hacker News Reader

Comment by ActorNightly | Hacker News Reader

Why not?

If you think about correctness of a program, (i.e for any combination of given input , it changes a state in a determinstic way, including no state change for invalid input).

Strict typing is one way to accomplish this. The cpu does not give a shit about types. It cares about memory registers and locations. The unique code built into the compliers/transpilers is the thing that validates the correctness of the program in this case.

You can move that code into the testing suite without relying on the complier, and just do testing. Generally, given competent programming skills, this takes about the same amount of time as designing a well structured program - your tests are pretty much your design document for the thing itself.

View on HN

This is a very anti-pragmatic way of looking at things in my opinion. The program is not a snapshot that exists in a vacuum. Most programs are going to grow over time and have things added and removed in various places by many people. They're going to have many interfaces and operations.

I think you're arguing that tests and types can both be used to check a particular case for correctness. Sure, this is true. However "moving type checking code into the test suite" means nothing—that would just be type checking.

When you make a code change, there's a difference in the kinds of feedback you get from your tests and your types. Tests usually cover business logic or stories—things that you want or don't want. Types ideally cover everything. They check every operation applied to a given piece of data. Of course types are rarely precise enough that they can catch every logic bug (e.g. strings with semantics not encoded in types, like email addresses).

This is just scratching the surface. You might just have to try out both to get a better sense of how they feel to work with.

So at one of my older jobs, we worked primarily with C code that ran on a mini linux box inside a plane, and interfaces with a sensor pacakge. We wanted to make sure that the software was 100% correct cause any errors would mean an aborted flight test

We basically ended up creating a tool+language spec that would let us define the mapping of input to output sequences. We wrote it in such a way where we sat with scientists and pretty much mapped all the possible cases that they could think of for valid inputs and what the code should produce.

Then this tool would basically write automated tests for us, in such a way as to not only test correct behavior, but also do combinations of inputs out of order, fuzz testing, and so on. We ended up making it also check memory state, to ensure that there was no memory leaks, and analyze the memory space for required data or data that should not be there.

In the end, whenever someone was developing anything for this software, they would basically just run the tests, and it would be very good at catching possible errors, mostly on the negative side (i.e for a fuzzed input, it would result in an output that should be an error).

We could have done the same thing with a typed language, but it would have to be very strict typing to the point of something like CoQ, and it would have taken us probably the same amount of time to write that.

Hey, that's awesome. Seems like a great case for verifying things that way! I'm thinking of different cases I think, where you've got something like a distributed system or a web application and it's just harder to fuzz. But I agree, that seems a lot more practical than formally verifying it when that's the kind of testing you need.

You can not test for the absence of behavior. You can design type systems to ensure the absence of specific behaviors.

What do you mean by absence?

Types [1] can only reason about categories of values, not about values. Tests and types do have an overlap, but the best option is both. Especially when combined with fuzzing, types can exclude large number of cases, making it even more efficient at covering a huge range of code paths.

[1] yeah, there are type systems like lean, coq that can do both, but the proving process is just currently not realistic for everyday applications

Reply on news.ycombinator.com