> programming work in the next decade will be done by logicians using something like TLA+

How is that not software engineering?