Programming in Lean, Agda, and Idris have been quite a revelation in terms of interactive type system exploration. Granted, they can be flakey at times (Lean especially), but it's a tantalizing glimpse at what could be around the corner. Hazel[1] is also a pretty exciting look at advancing the idea of 'programming with holes', as is Isomorph[2]. Lots of exciting things around the corner!

[1]: http://hazelgrove.org/

[2]: https://isomorf.io/