Isolating complexity is the essence of successful abstractions • Hacker News Board

Re: Isolating complexity is the essence of successful abstractions

#81

Post by suraci » Thu, Jan 23, 2025, 11:00 AM UTC

wavemode wrote: post #59

The author's assertion is true - complexity has to live somewhere. The nuance, though, is that all places complexity can live are not created equal. Let's take the example of memory management: by pushing that complexity into the type system, Rust forces the programmer to deal with it and design around it. At the expense of some performance, we could instead push this complexity into a runtime garbage collection syst…

IMO, cognitive load is the complexity of 'the scale of knowledge you need to build the solution (the problem space).'

However, complexity also comes from the solution itself — caching, microservice architecture, or even poorly chosen variable names.

So, complexity is irreducible, but it’s not a constant.

Certain solutions partition the problem space, thereby partitioning the complexity. This reduces the local complexity and, consequently, the cognitive load. However, the global complexity still remains and can even increase.

Re: Isolating complexity is the essence of successful abstractions

#82

Post by bluGill » Thu, Jan 23, 2025, 3:32 PM UTC

dlahoda wrote: post #79

bluGill wrote: post #75

Earlier quoted context omitted.

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)

> runtime asserts/expects

Those are not proofs. If you have a formal proof tool (I'm not aware of one for rust, but there is a lot of progress in this area) they feed and and sometimes tools can prove things. Though beware, there are limitations to this approach - sometimes they would have to solve the halting problem to say code is correct (though if they say code is wrong they are right), other times the problem is solvable only on a computer that doesn't exist yet.

Types and const are a form of formal proof - if you don't cast those away (I'm not sure what rust allows, particularly in unsafe). However there is a lot more potential in formal proofs. Rust's borrow checker is formal proof, and there are safe things you might want to do that the borrow checker doesn't allow because if it was allowed rust could no longer prove your code memory safe (a trade off that is probably worth it in most cases)

Re: Isolating complexity is the essence of successful abstractions

#83

Post by earth_walker » Thu, Jan 23, 2025, 5:25 PM UTC

drdeca wrote: post #71

hitchstory wrote: post #58

Earlier quoted context omitted.

>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 sati…

Good question - and there's been lots of work on this area. See for example property testing and fuzz testing, which can do something similar to what your second paragraph suggests.

You should be able to find a property testing library in your favourite language such as Hypothesis (python), Quickcheck (Haskell), Fastcheck (JS/typescript), etc.

Re: Isolating complexity is the essence of successful abstractions

#84

Post by steveklabnik » Thu, Jan 23, 2025, 5:30 PM UTC

bluGill wrote: post #82

dlahoda wrote: post #79

Earlier quoted context omitted.

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)

> runtime asserts/expects Those are not proofs. If you have a formal proof tool (I'm not aware of one for rust, but there is a lot of progress in this area) they feed and and sometimes tools can prove things. Though beware, there are limitations to this approach - sometimes they would have to solve the halting problem to say code is correct (though if they say code is wrong they are right), other times the problem is…

I agree with what you're saying, but some context:

> I'm not aware of one for rust, but there is a lot of progress in this area

https://github.com/model-checking/kani is probably the best known one, I believe there are a few others.

> (I'm not sure what rust allows, particularly in unsafe).

You can't "cast const away" in Rust, even in unsafe. That is, you can do it in unsafe, but it is always undefined behavior to do so. (I am speaking about &T and &mut T here, const T and mut T exist and you're allowed to cast between those, as they have no real aliasing requirements and are really just a lint.)

Re: Isolating complexity is the essence of successful abstractions

#85

Post by earth_walker » Thu, Jan 23, 2025, 5:33 PM UTC

dartos wrote: post #6

I don’t think I agree that either typescript nor rust successfully hide the complexity in their type systems. By the nature of type systems, they are tightly coupled with the code written around them. Rust has rich features to handle this coupling (traits and derives), but typescript does not.

Abstractions are a way to manage complexity - hiding things is only one way to do that. Deciding how to organize it, when and how to expose it, and when to get out of the way, are all important aspects of designing abstractions.

Re: Isolating complexity is the essence of successful abstractions

#86

Post by hitchstory » Sun, Jan 26, 2025, 5:51 PM UTC

drdeca wrote: post #71

hitchstory wrote: post #58

Earlier quoted context omitted.

>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 sati…

Jane logs in, enters her DOB which is 11/5/1998, does Y the result of which is Z.

Where X, Y and Z are very specific.

These example scenarios work well as a communication medium for discussing intended program behavior as well as translating well into tests.

>enumerate every possible combination

Whereas if you start doing this you will probably confuse your stakeholders.

Specific examples tend to make better specifications.

Re: Isolating complexity is the essence of successful abstractions

#87

Post by drdeca » Tue, Jan 28, 2025, 12:01 AM UTC

hitchstory wrote: post #86

drdeca wrote: post #71

Earlier quoted context omitted.

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 sati…

Jane logs in, enters her DOB which is 11/5/1998, does Y the result of which is Z. Where X, Y and Z are very specific. These example scenarios work well as a communication medium for discussing intended program behavior as well as translating well into tests. >enumerate every possible combination Whereas if you start doing this you will probably confuse your stakeholders. Specific examples tend to make better specific…

A “specification” which is based on just “the desired behavior in a few specific examples” seems to allow undesired behavior without it being clear whether said behavior is allowed by the spec.

That to me doesn’t seem like what a “specification” is.

Now, maybe having good examples is more important for business use cases than having a specification.

But I generally wouldn’t call it one.