Linear algebra

I'm having a kind of brainstorm here about linear algebra, mostly because my daughter is studying for her linear algebra final.  Here in Hungary, that means proofs - lots of proofs.  In America, it typically means problem-solving (actually, there's a separate problem-solving part of the class in Hungary as well, and she aced that).  To me, linear algebra means some useful concepts for machine learning and statistics.

Overall, the semantics of linear algebra should actually be pretty simple, right?  The semantics of mathematical techniques and concepts are strictly defined.  (I mean, the semantics of their application might not be so hairless, but still.)  So a semantic domain of linear algebra should include boilerplate and idioms for working with matrices in R and Python and C, graphing with gnuplot, and so on. Even the proofs of theorems should be formalized with CoQ in such a setup.  And of course all of it should map onto LaTeX and OpenMath definitions of the display math.

The presentation of such a semantic domain could be seen on a number of different levels, and in a sense, the presentation should be the definition - a sort of literate programming concept.  A book, in other words, about linear algebra that simultaneously defines the domain in terms of semantic structures that could be used to program software for linear algebra.

And that presentation would be a really useful book.  I have no idea at all how best to organize such a work, but it's a hell of a vision, isn't it?

Here are a few linear algebra notes gleaned from HNN just now.  I'm trying to find a specific linear algebra overview that I truly recall seeing on HNN, but I can't find it now, so ... maybe I dreamed it.

Primers and intuitive overviews are always nice.  Here's a great one.  And another.  Here's a primer I find a little intimidating.  And a blog post series on the toolbox provided by linear algebra.

A fantastic post by a guy who taught linear algebra that has nothing to do with linear algebra, but is a pretty decent way to run a math class.

Finally, what seems to be a decent set of notes.