So it could be [efficiently?] decidable if you forced the function specification to adhere to certain rules that ensured a standard, easily-comparable format?
It depends on how restrictive your "certain rules" are. It's quite possible to restrict things so much that functions will be comparable in terms of both structure and functionality. But usually that's way too much restriction.
Consider the example of writing a function that does the collatz sequence computation and another function that just returns one. How would you compare them? It will most likely return Equal but even the greatest mathematicians can't say for sure.
Now consider another example where you restrict the function definition to only include simple arithmetic (no control flows i.e. no conditionals no loops no function calls). A good CAS system can already simplify these functions and you can compare them quite easily (though not trivially).
On the other hand, if the rules are restrictive enough to stop the language from being Turing-complete, you could make it work.
There's an interesting design problem there: how do you make a language that's powerful and expressive enough to be useful but simple and restricted enough to solve problems like this reliably?
> There's an interesting design problem there: how do you make a language that's powerful and expressive enough to be useful but simple and restricted enough to solve problems like this reliably?
See theorem proving systems like Coq which use languages that are total. The majority of loops you write while coding obviously terminate (for item in items...) and Coq lets you prove more complex forms of looping terminate so it's not as restrictive as you'd think.
Coq and similar languages are definitely quite expressive, but they're still complex enough to involve non-trivial manual intervention. Verifying something with Coq is possible but it's hard; whole PhD theses have been written around verifying code for a single program. I know there is some proof-search-based automation available (ie auto), but I understand it's still pretty limited.
Coq, Agda and similar languages are restricted enough to make verification possible, but complex—and expressive—enough to make it very difficult to automate.
The opposite extent would be domain-specific languages that are very restrictive but still powerful enough for their domain. Designing languages like that would let us verify non-trivial properties fully automatically and can save a lot of work for the user, but we end up needing to design a language for each class of task that we care about.
As I said: it's an interesting design problem.
One recent addition to this is the Lean theorem prover, which tries to be similarly powerful and general as Coq but with more provisions for automation via the Z3 SMT solver. I haven't played with it myself but from what I've heard it's a very promising development in making formal verification more accessible to non-experts.
> Coq, Agda and similar languages are restricted enough to make verification possible, but complex—and expressive—enough to make it very difficult to automate.
Pretty much every theorem proving system out there is expressive enough to state whatever program property you want. You can't escape having to automate proofs though.
> Coq and similar languages are definitely quite expressive, but they're still complex enough to involve non-trivial manual intervention. Verifying something with Coq is possible but it's hard; whole PhD theses have been written around verifying code for a single program.
Yes, it's the most challenging aspect of programming I've ever tried. It's completely impractical and too expensive for most projects right now outside of domains where mistakes cost even more like aviation, medical devices, operating systems, CPU etc.
> The opposite extent would be domain-specific languages that are very restrictive but still powerful enough for their domain.
I'm not really sure what the sweet spot is to be honest or if there is one when you require full automation. Even non-linear arithmetic is undecidable (basically arithmetic where you're allowed to multiply variables together) so you quickly get into undecidable territories for what seem like basic properties. No clever language design idea is going to let you side-step that proof automation is hard which has been worked on for decades. Even writing program specifications requires a skillset most programmers will have to learn.
When you add restrictions to make equalities like this decidable, it usually means less things are equal to each other if that makes sense so the problem is being pushed elsewhere somewhat.
For example, Coq has decidable equality which is crudely described as "simplify both sides as much as possible and if they're syntactically the same then they're equal". So this could be equal depending on how you define plus:
plus(1, plus(1, x)) = plus(2, x)
but this wouldn't be:
plus(1, plus(1, x)) = plus(x, 2)
Long story but "plus" is usually defined by recursion on the first argument and when you put the "x" as the first argument the type checker cannot simplify "plus(x, 2)" any further so it isn't able to simplify both sides to the same form, therefore they're not equal. So this makes equality decidability but now things you intuitively think of as equal aren't equal.
What do you mean? You can write theorems that show plus is associative and commutative for example but that doesn't make the example I gave "equal" in Coq in the sense you normally mean. As I said, it's not intuitive as we're usually very loose in what we mean by "equal".
