Frankly I've been waiting a long time for someone to post exactly this pitch. I think that AI (and possibly CAD) is the biggest motivation for me wanting dependent types. As AI operates more broadly in software ecosystems and programming I want tools that can prove certain restrictions in an AI's model or its output in a far more rigorous way that what's currently offered by compilers. Combining that with differential swift my hope is these can also open doors to more bespoke learning architectures to solve specific problems, or entirely different architectures that aren't based just on feed-forward neural networks. For those concerned with adding complexity to the language, I would refer to this, "Our goals for Swift are ambitious: we want to make programming simple things easy, and difficult things possible." https://www.swift.org/ -- not trying to be dismissive of concern, just pointing out the goal should be to make that complexity progressively disclose for those who want it or need it.
Yet from what I'm reading, there's already some clear stepping stones that will get us closer to this vision without yet requiring universes and dependent types in the language, as pointed out. GADTs, const functions, everything codafi pointed out, and actually mainlining auto-diff itself. Not to mention generalizing keypaths to optics and including broadcasting (there was some mention of this in this thread Ongoing work on differentiable Swift - #16 by Troy_Harvey) and whatevers' left in the generics manifesto swift/GenericsManifesto.md at main · apple/swift · GitHub.
Is there good reason "Dependent Types & Universes" is the thing that should be tackled first? Makes me wonder if there's an evolution to the GenericsManifesto or a new manifesto that can accurately capture the 30k ft view of how these pieces should connect and lay out some relative prioritization. Maybe there's a way to split up some of these ideas to be spec'd out a bit and recombined into a larger viewpoint?
P.S. I really liked the straw man syntax discussed in the thread you posted by anachron and also was very excited about that conversation before it seemed to fade away.