5/16/2026 at 12:48:57 PM
"All Charity computations terminate" - Turing decidable it was.by dlahoda
5/16/2026 at 2:48:23 PM
I think it would imply that it is a Turing incomplete language. So, it would not be able to express certain programs, but all the computation you can represent is mathematically shown to reduce to a termination point.by vinnyhaps
5/16/2026 at 3:27:46 PM
IIRC they do some stuff with f co algebras. Which if I understand it is effectively doing things like "hey here's a generator that produces an infinite number of the number 1, but the only way to evaluate it is via a take with a finite number".I know with idris there is also a progress evaluator for otherwise general recursion that proves that your input is always "getting smaller". Not sure if charity has the same deal or not.
Regardless, it isn't turning complete, but the interesting part is how far you can get in a sub turing environment.
by Verdex
5/16/2026 at 7:39:04 PM
Afaik there was Turing limited kind of language which had Turing decidable fragments https://www.microsoft.com/en-us/research/wp-content/uploads/...afaik it is still in relatively active development
by dlahoda
5/16/2026 at 7:40:24 PM
Rust macro compiling function to NPU kernel likely is Turing decidable "fragment".by dlahoda