Abstractions

It is by generalized abstraction of what is repeatedly observed, that the concepts are introduced.

Anything is defined in terms of someting which is already defined (known and understood).

Analyzing which terms are used in a definiton of, say, an axiom, tells a lot about it.

So we have to understand the terms in which our functions (or procedures) are defined. We could even use yet unimplemented or even undefined, still abstract terms in prototyping our high-level definitions. This is what is behind the ABC – Always Be Compiled – principle. The details are still undecided or unimplemented yet. The undefined expression in Haskell and ??? in Scala are exactly for that.

This is how one could prototype ADTs (public interfaces) and modules first (using a converging process of trial and error). This is not the waterfall, this is a “spiral” of top-down-then-bottom-up gradual refinements.

Just as Dijkstra stated back then, “there is a stromg analogy between using a named operation (function) in a program regardless of “how it works” and using a theorem regardless of how exactly it has been proved”.

We also name concepts to “invoke” them in our minds. Mathematics has been developed this way.

There is an abstraction involved in naming (denoting) an operation and using it on accout of what it does (specification) while completely disregarding “how it is impelemented”.

Using “public” imperative interfaces according to an informal, ill-defined specification and hoping for the best is what a modern programming at large is nowadays.

It is so much better in mathematics, where everything is defined precisely, bound to “standard” symbols and never change.

\(a + b = b + a\)

Using symbols as a generalization from actual values.

Using symbols to denote (name) operations, such as \(+\).

Universal qualifier \(\forall\)

Recursion for repetition (looping), inspired by mathematical induction.

Partitioning based on properties (Sets).

First-order logic (predicates on sets).

Interfaces (Sets of possible operations).

Abstract Data Types.

Type-classes (ADTs for ADTs).

Abstraction barriers (atoms as building blocks of Life itself).

“Dots and arrows” of the Category Theory.