[stack] Motivations to embrace decidable type systems

One motivation for this work was to broaden the range of functions which can be investigated by looking at their type, which can be useful to see their effect. Another was to allow the programmer to provide additional constraints. I also hoped that the type would form a basis for proving properties of any function, using denotation provided by the programmer. I did not want the type system to restrict which functions or algorithms could be considered. We should be free to get a function working empirically, then prove its correctness.

And another was to use inheritance polymorphism, mix in native objects from Java or C# and type their interfaces, and investigate uniqueness types in concatenative languages. Perhaps an undecidable type system is not really necessary for this. But I wanted a type system for experimental programs that might be rejected by conventional type systems.

I do not expect that there is any automated (unguided) procedure to check, for instance, whether two type formulas are equivalent in this system. (Is this what decidable type inference means?)