I just feel an existential angst, are we damned to keep reinventing the same wheel? Static contracts and proofs are basically solved for industrial use in SPAR

I just feel an existential angst, are we damned to keep reinventing the same wheel? Static contracts and proofs are basically solved for industrial use in SPARK, yet somehow we keep reinventing. Is computer science really engineering? We don’t stand on the shoulders of giants, every new generation has the urge to invent a leave a mark. This in itself is great, except that, in contrast to other branches of engineering (say mechanical, or structural) previous know how is ignored and disregarded. Perhaps there is too much of it, and SNR these days is too low, impossible to be held in one’s head. Perhaps it’s easier these days with LLMs to survey what’s done. Yet the slop waves keep crashing on us. We have seen this with dbs. The relational model layed the foundations. Yet periodically a new craze emerges. Everyone’s chases the latest cool new thing, until the ugly warts that were know to be there decades ago resurface and become real blockers (looking at you mongo). Yet another post about program proofs, yet no mention of the only industrial strength, actually practical and pleasant to use formal verification language: SPARK.