One of the best authorities on that concept is Djikstra - they actually formally proved a few full algorithms and also provided a lot of guidance on how to prove others. It’s not something you’ll see… well, probably ever… but it’s a very interesting approach to program design. Dijkstra imagined a world where all programmers would be writing formal proofs of correctness before authoring a single line of code… that’s a neat world, I’d love to see it… but it’s also incredibly burdensome so our tech explosion would likely be happening a lot slower.
Being able to factor algorithms like algebraic equations is really neat.
I’ve never been able to wrap my head around proofs of algorithms, but I love the idea.
One of the best authorities on that concept is Djikstra - they actually formally proved a few full algorithms and also provided a lot of guidance on how to prove others. It’s not something you’ll see… well, probably ever… but it’s a very interesting approach to program design. Dijkstra imagined a world where all programmers would be writing formal proofs of correctness before authoring a single line of code… that’s a neat world, I’d love to see it… but it’s also incredibly burdensome so our tech explosion would likely be happening a lot slower.