Microsoft's efforts in Z3 and Lean to make IDEs interactive theorem provers is going to change how we code. I'm curious which will be the first to adopt FPGAs and Micron Automata style processors in memory.