[antpls]

> The thing to realize is that theorem proving is not a business goal in most cases. What you care about is being able to deliver software that works well in a reasonable amount of time. Sure, you might end up with a binary search bug in your code that goes unnoticed for 10 years, but clearly the world didn't stop because of that, and people have successfully delivered many projects in Java despite that bug that work perfectly fine.

I agree with you on that part. However, if the whole stack of computer technologies were more reliable, we would maybe think about new business usecases that we subconsciously dissmised because of lack of trust in current technology.

[yogthos]

It's basic cost/benefit analysis. At some point you end up with diminishing returns on your effort that are simply not worth the investment.

Also worth noting that nobody has been able to show that static typing leads to more reliable code in practice https://danluu.com/empirical-pl/

Claiming that to be the case putting the cart before the horse. A scientific way to approach this would be to start by studying real world open source projects written in different languages. If we see empirical evidence that projects written in certain types of languages consistently perform better in a particular area, such as reduction in defects, we can then make a hypothesis as to why that is.

For example, if there was statistical evidence to indicate that using Haskell reduces defects, a hypothesis could be made that the the Haskell type system plays a role here. That hypothesis could then be further tested, and that would tell us whether it's correct or not.

This is pretty much the opposite of what happens in discussions about static typing however. People state that static typing has benefits and then try to fit the evidence to fit that claim.

[antpls]

I agree with you, there is no much data about the effectiveness of more rigorous software development tools. It's clearly a research topic.

My intuition is that, with advances in robotics and AI, we may see the need of more robust logical systems. At some point, mathematicians and algorithmicians may use those tools to prove new concepts, which they will be able to share and valid more quickly, which then will percolate into software engineering more quickly.

Beyond software engineering, the expirements with theorem provers may lead to new ways of exchanging information, such as news, mathematics and legal documents. There are inspirations to take from the formalizations created in theorem provers for applying automated reasoning in more domains than just programming (imho)

Edit : Intuitively, it has do to with building trust in the algorithms and informations we share at light speed. With more validated building blocks, we may explore more complex systems. Accelerating trust between different entities can only lead to plus value, I guess. That's all very abstract tho

Edit 2 : too put it in even fewer words, theorem provers may be more about collaboration than just pure technical engineering

[yogthos]

To be honest, I think that once we have advances in AI there will come a point where you won't really be doing the kind of programming that we do today by hand. You'll have an AI assistant whom you'll give queries that are close to natural language, and it will figure out how to implement them for you. I can see that coming within a few decades for many kinds of applications such as your typical CRUD apps.

[antpls]

In such an hypothetical world, the "typical CRUD application" may just not even exist anymore.

I was talking about advances in consumer drones, autonomous cars, and personal robots, such as SpotMini from Boston Dynamics. More autonomous embedded systems evolving around us means different needs in term of safety in software development.

AI will have to explain the reasoning of their decisions (prove they did right) in natural language. The humans who do that in our world are scientifics, politicians, lawyers and mathematicians. Those people use a specific kind of natural language, with domain specific words to communicate. Theorem provers in software engineering are a step forward that direction imho

[yogthos]

Sure, you wouldn't really interact with a computer the way we do now once you have AIs that can understand natural language. It would be more like having a personal secretary.

I don't think theorem provers are actually the way to get there though. AI systems are probabilistic in nature, and neural nets are self-organizing. One of the biggest problems is that it's really hard to tell how such a system arrives at a decision. The human brain itself is not based on formalism, and we find formal thinking to be very challenging. It's something that needs to be trained, and doesn't come to most people naturally. Our whole cognition is rooted in heuristics.

[antpls]

> One of the biggest problems is that it's really hard to tell how such a system arrives at a decision. The human brain itself is not based on formalism, and we find formal thinking to be very challenging

So far, "neural networks" in AI is a fancy name for what is nothing more than a giant equation system with many parameters. It's not even close to a biological, actual self-organizing, neural networks. It's closer to a weather model prediction.

The human brain is not based on formalisms, so let's create an AI that helps the human brain's weakness. Maybe we shouldn't try to replicate the human brain capacities, but rather create a new "form of life" complementing our biological skills.

So far, theorem provers, with expert systems, are the only works I'm aware of about systematically explaining reasoning and decisions.