Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Isolating complexity is the essence of successful abstractions

v5.chriskrycho.com

Post reply on HN
Print view View original

71–80 of 87 posts

Re: Isolating complexity is the essence of successful abstractions

#71

Post by drdeca »

hitchstory wrote: post #58
youerbt wrote: post #41

Earlier quoted context omitted.

I believe you (other than tests being specifications, they are examples at best). But that doesn't change the fact that TDD looks more adopted in untyped languages, and that deserves an explanation. Mine is that a lot of potential errors (typos, type mismatches) don't need to be exercised by running code in typed language. Yours is... well, you don't really address it.

>I believe you other than tests being specifications If you're not, that suggests you're not doing them right which in turn suggests why you might have an issue with them...

How would you make a test a specification?

I suppose you could do something like, enumerate every possible combination of inputs and check that some property holds for all of them. Or, maybe you could instead randomly select a number of combinations of inputs and check that a property holds for each of those random combinations, but that wouldn't be guaranteed to find the inputs for which the specification isn't satisfied.

I guess maybe if the test passed to the function to be tested, mock values, such that the function is effectively evaluated symbolically (where any branching that depends on the inputs to the function, would maybe have the mocked object specify what the result of the conditional should be, with different tests for different cases?) ?

Or.. Can you explain how you write tests such that they truly function as specifications?

Re: Isolating complexity is the essence of successful abstractions

#72

Post by eptcyka »

bluGill wrote: post #49
youerbt wrote: post #34

Earlier quoted context omitted.

> That also explains why TDD is more popular in say Ruby or Python vs. Java. I'd say that TDD being more popular in untyped languages speaks against TDD, as it hints that maybe some of its benefits are covered already by a type system.

You did clarify latter a bit, but this cannot stand unchallenged. TDD and tests solve different problems from types and so are valuable for that. Tests assert that no matter what you change this one fact remains true. Types assert that you are using the right things in your code. I don't think it is lack of types at fault for untyped languages liking TDD (though I miss types a lot). I think it is there is no way to f…

The biggest proponents of TDD I’ve seen are only capable of writing code that one cannot trust in the absence of tests. Writing tests is good, striving for 100% coverage contorts code in ways that are detrimental to robustness and correctness.

Re: Isolating complexity is the essence of successful abstractions

#73

Post by timewizard »

elcritch wrote: post #37
timewizard wrote: post #21

> Complexity has to live somewhere. If you are lucky, it lives in well-defined places. This whole section makes me think of construction which has similar abstraction and hidden complexity problems. It strikes me that they solve it by having design be entirely separate from implementation. Which is usually the corner where all our luck as software developers inevitably runs out. Our methods are still rather "cowboy."…

To be fair to our field fields like construction have literal millennia of history and development to figure out the best patterns. Even then it’s still evolving. It’s crazy to see what we’re capable of building now vs even 15 years ago.

Construction is not built on a machine that has had exponential growth for those 15 years. So our capabilities have expanded but it seems like our problems have as well.

Re: Isolating complexity is the essence of successful abstractions

#74

Post by tshaddox »

dlahoda wrote: post #39
youerbt wrote: post #34

Earlier quoted context omitted.

> That also explains why TDD is more popular in say Ruby or Python vs. Java. I'd say that TDD being more popular in untyped languages speaks against TDD, as it hints that maybe some of its benefits are covered already by a type system.

types are just autoverified logic. tdd just tests logic which cannot be typed in given type system. in lean4 one can type a lot(dependant types to test integration shapes and proofs are proptests).

It's worth nothing that type checking can also verify things that cannot reasonably be verified by tests. Things like exhaustiveness checking ("you handled every possible value of this enum") or, even simpler "you didn't attempt to access a property that does not exist on this object."

Re: Isolating complexity is the essence of successful abstractions

#75

Post by bluGill »

Tainnor wrote: post #60
bluGill wrote: post #51

Earlier quoted context omitted.

TDD also asserts that if you make a change you don't break anything. Most programs are too complex to keep all behavior in your head so sometimes what looks like an obvious change breaks something you forgot about. Types won't tell you because you adjusted the types, but the test will tell you. (if you have the right tests of functionality - a very hard problem outside the scope of this discussion)

The person you're replying to mentioned Lean4. In such a language, types can definitely assert that a change didn't break anything, in the sense that you can write down the property you want as a type, and if there is an implementation (a proof), your code satisfies that property. Now, proofs can be often devilishly hard to write whereas tests are easy (because they're just examples), so in practice, types probably w…

Proofs are impossible in many cases because nobody really fully understands the requirements, they are sort of working them out as they go. (and in any case they will change over time). That might be what you meant by devilishly hard to write.

Tests let you instead say "with this setup here is what happens", and then ensure that whatever else you change you don't break that one thing.

To my knowledge nobody has scaled proofs to very large problems. I still think proofs should have a place in better code, but I can't figure out how to prove anything in my real world code base. (I could probably prove my languages basic containers - something that itself would be valuable!)

Re: Isolating complexity is the essence of successful abstractions

#76

Post by bluGill »

eptcyka wrote: post #72
bluGill wrote: post #49

Earlier quoted context omitted.

You did clarify latter a bit, but this cannot stand unchallenged. TDD and tests solve different problems from types and so are valuable for that. Tests assert that no matter what you change this one fact remains true. Types assert that you are using the right things in your code. I don't think it is lack of types at fault for untyped languages liking TDD (though I miss types a lot). I think it is there is no way to f…

The biggest proponents of TDD I’ve seen are only capable of writing code that one cannot trust in the absence of tests. Writing tests is good, striving for 100% coverage contorts code in ways that are detrimental to robustness and correctness.

I like to think I'm better than that. Who knows though.

I'm also against measuring coverage - I've never seen anything useful to do with the measure so why bother.

Re: Isolating complexity is the essence of successful abstractions

#77

Post by rapjr9 »

One of the problems with abstraction is that while it hides complexity, it makes changes that must reach into that complexity difficult. Abstraction is great if the code is never going to change again. If the people using the code want new features, then abstraction is a barrier. Getting around the abstraction barrier makes the code more complex. You have to think about the entire life cycle of the code, not just what looks pretty when you first write it. Most developers have no idea what their code will be used for 5 or 10 years into the future. As an example people have been trying to abstract away the complexity of network connections for decades, without a lot of success in keeping the complexity hidden. Someone always needs direct intervention in a layer in the network stack to make their product work right.

Re: Isolating complexity is the essence of successful abstractions

#78

Post by sevensor »

chuzz wrote: post #32

That's why Typescript/Python optional typing hit the best balance for me. Coding in duck-typed language is generally fine when your test suite is as fast and frequent as a type checker. That also explains why TDD is more popular in say Ruby or Python vs. Java. Speaking of Java, the problem with types is when you try to reify every single problem you encounter in your codebase. By the way, python has structured types…

The article makes one of my favorite points about types: types aren’t there to constrain you; what they constrain is the complexity of the program.

Re: Isolating complexity is the essence of successful abstractions

#79

Post by dlahoda »

bluGill wrote: post #75
Tainnor wrote: post #60

Earlier quoted context omitted.

The person you're replying to mentioned Lean4. In such a language, types can definitely assert that a change didn't break anything, in the sense that you can write down the property you want as a type, and if there is an implementation (a proof), your code satisfies that property. Now, proofs can be often devilishly hard to write whereas tests are easy (because they're just examples), so in practice, types probably w…

Proofs are impossible in many cases because nobody really fully understands the requirements, they are sort of working them out as they go. (and in any case they will change over time). That might be what you meant by devilishly hard to write. Tests let you instead say "with this setup here is what happens", and then ensure that whatever else you change you don't break that one thing. To my knowledge nobody has scale…

i am coming from rust. writing a lot of narrowing wrappers/type states/proptests/const and runtime asserts/expects of possible proofs. i am targeting to do these first.

for big things wiring many things together, will use normal tests(given lean4 allows to reflect on io graph, i guess can have some fun here too)

Re: Isolating complexity is the essence of successful abstractions

#80

Post by Tainnor »

bluGill wrote: post #75
Tainnor wrote: post #60

Earlier quoted context omitted.

The person you're replying to mentioned Lean4. In such a language, types can definitely assert that a change didn't break anything, in the sense that you can write down the property you want as a type, and if there is an implementation (a proof), your code satisfies that property. Now, proofs can be often devilishly hard to write whereas tests are easy (because they're just examples), so in practice, types probably w…

Proofs are impossible in many cases because nobody really fully understands the requirements, they are sort of working them out as they go. (and in any case they will change over time). That might be what you meant by devilishly hard to write. Tests let you instead say "with this setup here is what happens", and then ensure that whatever else you change you don't break that one thing. To my knowledge nobody has scale…

> That might be what you meant by devilishly hard to write.

No, that's a separate problem. I agree that we don't always know what we need our code to do very precisely - although I think we could still increase the number of known invariants/properties in many situations - but even when you do, a proof is often hard to write.

Proofs also typically have the problem that they're not refactoring-proof: if you change the implementation of function f (but it still does the same thing), tests won't have to change, but a proof would have to be rewritten (the type would stay the same though).

Post reply on HN