Jimmy Koppel

This is such a great quote, and helps explain what is a good abstraction.

Because CRDTs have been in the zeitgeist a lot lately, I want to pick them as an example of a "good" abstraction.

CRDTs have mathematical properties which can be described and understood independently of a specific implementation. And importantly, you can judge whether an implementation is correct with reference to these abstract rules.

This means that when using a CRDT, you largely can treat it as a reliably-solved problem. Once you understand the concepts, and work out how to use the library you've picked, you don't have to think about the details. Though that doesn't mean sometimes the behaviour can be surprising:

https://www.moment.dev/blog/lies-i-was-told-pt-1

TCP and HTTP are great examples too, though interestingly I don't know if they rely on mathematical definitions so much as just being extremely widespread to the point that reliable implementations are available anywhere you care to write code.

I like this article which also leans on the Dijkstra quote:

https://www.pathsensitive.com/2022/03/abstraction-not-what-you-think-it-is.html?m=1

Mutual single recursion is still a loop; you just pick where you want to cut the cyclic dependencies to return to the top. In the worst case, you can put a `switch` in the loop and track what state you're in, although that's gross (you have to keep the union of all variables that might be used in each state).

Multiple recursion, like in `fib n = fib (n - 1) + fib (n - 2)`, is more general than loops... in a world without higher-order functions. You can make such a function tail-recursive by doing the continuation-passing transform, which basically just makes the stack explicit. (You'd then want to "defunctionalize the continuation" [0] to clean up.)

(I've actually done this in Java! Writing the multiply-recursive solution is sometimes a lot easier to do (and verify); transforming it into an iterative solution mechanically exposes a lot more hidden details, but you still have your recursive solution you can test and compare against.)

[0] http://www.pathsensitive.com/2019/07/the-best-refactoring-youve-never-heard.html

I bailed on high school math, thinking I'm math dumb.

In my late 20s I decided to try again, but jumped straight into calculus. And at first regretted that decision. However, I got lucky by stumbling upon this book:

https://www.amazon.com/Calculus-Made-Easy-Silvanus-Thompson/dp/0312185480

It "reads" like a book, with the ideas given context. I had an "ok" connection with Algebra, and the book explained the rest well enough for me.

In school, the textbooks were loaded with symbols, but not enough description -- I guess they relied on bored teachers making minimum wage to do that part. I went to a school with poor academic showings (but connections to state superintendent of ed got them a grant for football facilities).

Coincidentally, this book goes well with the technique described here:

http://www.pathsensitive.com/2018/01/the-benjamin-franklin-method-of-reading.html

> So.... this is just a fancy name for the advice "give your functions a name"?

Not quite: "defunctionalization" is a name for replacing functions with not-functions (data structures). (And IMO it's the most unfancy name one can give to that activity, as the name literally just indicates "removing functions"... I can't think of a less fancy name for it: maybe "un-function-ize"? But that's pretty much the same as "defunctionalization".)

BTW I recommend reading the 3 linked articles in this order:

1. https://blog.sigplan.org/2019/12/30/defunctionalization-everybody-does-it-nobody-talks-about-it/

2. http://www.pathsensitive.com/2019/07/the-best-refactoring-youve-never-heard.html (with accompanying video)

3. https://www.gresearch.co.uk/article/defunctionalisation/ (this one actually shows how you can incrementally adopt this)

Here is a counter argument: http://www.pathsensitive.com/2018/10/book-review-philosophy-of-software.html

My summary would be: The spec must cover all possible implementations so it is usually larger than the most simple one.

An example from there:

> The authors of SibylFS tried to write down an exact description of the `open` interface. Their annotated version of the POSIX standard is over 3000 words. Not counting basic machinery, it took them over 200 lines to write down the properties of `open` in higher-order logic, and another 70 to give the interactions between open and close.

> For comparison, while it’s difficult to do the accounting for the size of a feature, their model implementation is a mere 40 lines.

Thanks for the detailed break-down and the links!!

> which are pretty much always mathematically uninteresting), then...absolutely! SAT/SMT are at the core of constraint-based synthesis.

Wow this is super cool to know!

> http://www.pathsensitive.com/2021/03/why-programmers-shouldnt-learn-theory.html

This would definitely help to kickstart my journey in program synthesis:)

> "egg: Fast and Flexible Equality Saturation"... It uses code trees, which I read about a few months earlier in the Handbook of Automated Reasoning
> http://cubix-framework.com/
> https://egraphs-good.github.io/
> https://people.csail.mit.edu/asolar/
> https://github.com/microsoft/prose

These stuff are super cool! Really appreaciate it!