If Socrates met Linus Torvalds, what would they talk about? How much math should be bundled into a good programming language? Can compiler resolve an argument and prove, that someone is right?

Trough semantics of code, that we write every day, when looking carefully, one can see foundations of logic and science, that has been build more than 2000 years ago. Why does it matter, and how can we leverage this enormous power to make our code safe and sound in languages with advanced type systems, like Typescript and Scala.