I'm optimistic that improved proof search using modern AI can make working with dependent type systems much more productive and practical.

A future programmer may be spending more time formally describing the invariants of the system.