Where is the formal semantics of Data Analysis Expressions (DAX) documented?

Question

The expressive power of Microsoft’s Data Analysis Expressions (DAX) is really amazing. It is very useful to me … but after several months of practice I am still not fully confident of what my expressions will yield.

Usually when learning a new language I start with a tutorial, then read the user’s manual and then consult formal details in the reference guide. With DAX there are plenty of tutorials, in the form of textbooks, websites, blogs …. but if you want to go in more depth, all the sources I’ve seen so far are informal and just advice to “learn by practice”. Even the official reference by Microsoft , or the excellent https://dax.guide/ site, just give verbal explanations of DAX functions, but do not precisely explain what is a “context switch”, a “table filter” or other constructs.

Part of the confusion seems to come from the fact that DAX is often presented as a “functional language”, and is often paired with M, another language from Microsoft for expressing steps of data extraction and transformation. M is a truly functional language and has a very well-written formal specification. By contrast, DAX only has a functional syntax at the surface, but the semantics is not functional at all : DAX functions are evaluated within an implicit context, and many functions modify that context.

In a truly functional language, the result of a function only depends on the input values; and each argument to the function is computed independently before calling the function. In DAX it is very different; my gross understanding of it is as follows :

1. There is an implicit data model, which consists of tables and relations
2. Each table has an implicit set of reachable columns, which is the union of columns from all related tables
3. There is an implicit filter context, which is an assembly of Boolean conditions on reachable columns
4. Some of the DAX functions do not return a result, but they temporarily modify the implicit data model (for ex. CALCULATETABLE, USERELATIONSHIP), or temporarily modify the implicit filter context (for ex. FILTER, ALL).
5. Some functions quote expressions in some of their arguments, in the sense of LISP QUOTE. So for example the second argument in SUMX(table, [m1] * [m2]) does not mean “compute [m1], compute [2], multiply them and pass them to SUMX”; it rather means “create a new quoted expression ‘([m1] * [m2]), and pass that expression to SUMX which will iterate over the table, modify the implicit context at each row, evaluate the expression in that modified context, and then sum up the whole result”.
6. Some functions modify their arguments through syntactic sugar rules; for example CALCULATE(table, [column]=99) is a shortcut for CALCULATE(table, FILTER(ALL(table[column), [column]=99)).

So this is quite different from a functional language!

Of course the presentation above is just a very general direction for approaching a precise description of DAX semantics; it would need to be refined in full detail.

Is that way of seeing things correct ? Is there any published reference that already describes DAX at this level of precision ?