Where are cutting edge type systems at for statically verifying the “dimensionality” of computations? I remember a long time ago reading about a language from

Where are cutting edge type systems at for statically verifying the “dimensionality” of computations? I remember a long time ago reading about a language from sun called “fortress” which was going to include the option of assigning units to values in such a way that scientific domain model operations could be defined via a kind of type-sugar ... seems like that technology would work really well for ML (and data science in general) if it were effective. I remember reading some lengthy hype about fortress and then never hearing about it again ...