> The real future though is theorem proving systems, and generating code from them.
I've heard the same thing about model-driven development 25 years ago. Outside of some very small niches, it's pretty much dead now.
> But theorem proving systems that embrace the full spectrum of abstract and correct thought.
And here's where reality and the ideal world collide: the vast majority of applications consists of incomplete models (in that data and/or understanding of the problem are incomplete), quickly shifting goals, and pressure to release.
Theorem proving systems offer nothing that helps with this class of software - abstract and correct thought sounds marvellous in an academic environment or if you have unlimited budget to hire top talent and perform thorough analysis.
In practice, however, your typical line-of-business application is faster, cheaper, and well-enough programmed using traditional languages and a healthy dose of best-practises.
Optimisation and platform support are another area where a TPS won't be very useful. Every hardware has its quirks and workarounds are required to get the best performance or avoid pitfalls. These aren't easily expressed (and identified) using abstract thought and models.
Last but not least, no sane company is going to just throw away decades worth of investment in applications, libraries, and (software-)infrastructure just for a nebulous promise of what basically boils down to smarter and better staff with the right tools.
Theorem proving systems have their place and that place might get bigger in the future, but they're most certainly not the panacea of all software development.
The "generating code from them" brings the bad vibe of useless UML tools with it, but I put it in there anyway, because that's how it is going to be.
There is room for "experimental" programming of course, where you experiment with stuff and you are glad that you get it somehow working in the first place. But should stuff that peoples lives depend on depend on experimental software like that? No. And as software more and more becomes part of our lives, I don't see much software for which that attribute does not hold.
I've heard the same thing about model-driven development 25 years ago. Outside of some very small niches, it's pretty much dead now.
> But theorem proving systems that embrace the full spectrum of abstract and correct thought.
And here's where reality and the ideal world collide: the vast majority of applications consists of incomplete models (in that data and/or understanding of the problem are incomplete), quickly shifting goals, and pressure to release.
Theorem proving systems offer nothing that helps with this class of software - abstract and correct thought sounds marvellous in an academic environment or if you have unlimited budget to hire top talent and perform thorough analysis.
In practice, however, your typical line-of-business application is faster, cheaper, and well-enough programmed using traditional languages and a healthy dose of best-practises.
Optimisation and platform support are another area where a TPS won't be very useful. Every hardware has its quirks and workarounds are required to get the best performance or avoid pitfalls. These aren't easily expressed (and identified) using abstract thought and models.
Last but not least, no sane company is going to just throw away decades worth of investment in applications, libraries, and (software-)infrastructure just for a nebulous promise of what basically boils down to smarter and better staff with the right tools.
Theorem proving systems have their place and that place might get bigger in the future, but they're most certainly not the panacea of all software development.