@neauoire :: (oops broke that one reply by accident)
Interested in what ideas you explore within Tal's limits. FP languages have the advantage of a strong type system and pattern matching. If your type is finite and each step reduces the given inputs to their base cases, you can say confidently that "this loop terminates".
Idris does this, but it also means some finite functions can't be statically resolved and are marked as partial.
@CapitalEx I'm an absolute beginner when it comes to building type systems, so this is all fresh to me.
I've been going through the handlful of papers and blog posts on types/concat languages. This morning @toxi gave me a bunch of very interesting links on the topic: https://merveilles.town/@toxi@mastodon.thi.ng/110362257067437570
I'll keep reporting my findings, I've started a stub on the topic here: http://wiki.xxiivv.com/site/type_systems.html