Right, exactly! The theorem doesn't forbid the possibility of software that decides properties of some programs (including many useful properties for many useful programs).
This frustrates me a lot too-- I view it as an example of a general peeve of mine that people read too much into formal results often in a pretty cult like manner.
An example I like to use is that many people seem to believe that there is no reason to use anything other than the obvious greedy approximation algorithm for the minimal set cover problem because of a celebrated result in approximation theory that shows that no algorithm can achieve a better worst case approximation gap. Last I checked, the Wikipedia article-- for example-- pushes people in that direction.
It turns out in practice, however, on many problem cases the obvious greedy algorithm is pretty bad and simple heuristics on top of it do a LOT better. People are mistaking worst case with "average" or "typical" case.
In the problem space we're discussing here with Simplicity though, there are cases where undecidable isn't really an option: For example, if the consensus rules of a system impose execution cost limits, the result of evaluating the costs can't permit "undecidable", and so it's arguably better to work from a framework which guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
> it's arguably better to work from a framework which
guarantees that it won't be by construction... rather than attempting a game-of-operation where minor modifications to your program might seemingly randomly knock into undecidable-land.
I presume that a programming language is a compromise between expressiveness and decidability. Cost estimation feature is
definitely a good one until having that feature stops you from being able to develop your business logic in a convenient-enough manner.
Regarding the latter, I am not convinced that Simplicity is a nice fit.
