This is not actually a problem for total languages, which simply model these kin...

		Rusky 20 days ago \| parent \| context \| favorite \| on: Lean proved this program correct; then I found a b... This is not actually a problem for total languages, which simply model these kinds of processes using corecursion/coinduction/codata.