Ada does this too

Posted Feb 13, 2025 15:13 UTC (Thu) by Wol (subscriber, #4433)
In reply to: Ada does this too by daroc
Parent article: Maintainer opinions on Rust-for-Linux

> You are of course right in general; the price that Idris and Agda pay for being able to say that some programs terminate is that the termination checker is not perfect, and will sometimes disallow perfectly okay programs. So I don't think it's necessarily a good idea for Rust to add termination checking to its type system, but it is technically a possibility.

Can't Rust have several checkers? If any one of them returns "okay", then the proof has passed and the code is okay. The programmer could then also add hints, maybe saying "run these checkers in this order", or "don't bother with these checkers", or whatever. So long as the rule is "any positive result from a checker is okay", that could reduce the checking time considerably.

Oh - and I don't know how many other languages do this sort of thing, but DataBASIC decrements -1 to 0 to find the end of an array :-) It started out as a "feature", and then people came to rely on it so it's standard documented behaviour.

(I remember surprising a C tutor by adding a bunch of bools together - again totally normal DataBASIC behaviour, but it works in C as well because I believe TRUE is defined as 1 in the standard?)

Cheers,
Wol

Running several checkers instead of one

Posted Feb 13, 2025 15:34 UTC (Thu) by farnz (subscriber, #17727) [Link] (5 responses)

It's not the runtime of the checker that's the problem; it's that we cannot write a checker that definitely accepts or rejects all reasonable programs. The underlying problem is that, thanks to Rice's Theorem (a generalisation of Turing's Halting Problem), a checker or combination of checkers can, at best, give you one of "undecided", "property proven to hold", or "property proven to not hold". There's two get-outs we use to make this tractable:

We treat "undecided" as "property proven to not hold", and reject programs where the desired properties don't hold, or where it's undecided.
We work to minimise the amount of code that falls into "undecided"; we can't make it zero, thanks to the theorems proven by Turing and Rice, but we can reduce it to "things that a skilled human would understand why they can't make that work".

If we could ensure that "undecided" was small enough, we'd not have a problem - but the problem we have is that all known termination checkers reject programs that humans believe terminate.

Running several checkers instead of one

Posted Feb 13, 2025 18:01 UTC (Thu) by Wol (subscriber, #4433) [Link] (4 responses)

That's not what I'm getting at, though. We might have three or four different checkers, which return different subsets of "I can prove this code".

It only takes one checker to return success, and we know that that Rust code is okay. So if we know (or suspect) which is the best checker to run, why can't we give Rust hints, to minimise the amount of checking Rust (has to) do. Which then means we can run more expensive checkers at less cost.

Cheers,
Wol

Running several checkers instead of one

Posted Feb 13, 2025 18:31 UTC (Thu) by daroc (editor, #160859) [Link] (2 responses)

Sure, but there's a mathematical proof that any set of checkers you can make will have some programs that they can't decide. It's not just a matter of finding the right one.

So the tradeoff will always be between not being able to check this property, or being able to check it but rejecting some programs that are probably fine.

That said, I do think there is a place for termination checking in some languages — the fact that Idris has it lets you do some really amazing things with dependent typing. Whether _Rust_ should accept that tradeoff is a matter of which things it will make harder and which things it will make easier, not just performance.

Running several checkers instead of one

Posted Feb 14, 2025 15:12 UTC (Fri) by taladar (subscriber, #68407) [Link] (1 responses)

Maybe there is also a place for termination checking that doesn't cover the entire program? It could limit where you have to look for bugs similar to unsafe blocks or the way test coverage is displayed.

Uses of termination checking

Posted Feb 14, 2025 15:27 UTC (Fri) by farnz (subscriber, #17727) [Link]

Idris has both as part of its totality checker; a function can be partial (in which case it may never terminate or produce a value - it can crash or loop forever) or total (in which case it must either terminate for all possible inputs, or produce a prefix of a possibly infinite result for all possible inputs).

Idris then uses this to determine whether it can evaluate a function at compile time (total functions) or whether it must defer to runtime (partial functions). This becomes important because Idris is dependently typed, so you can write a type that depends on the outcome of evaluating a function; if that function is total, then the type can be fully checked at compile time, while if it's partial, it cannot.

Running several checkers instead of one

Posted Feb 14, 2025 11:02 UTC (Fri) by farnz (subscriber, #17727) [Link]

If you run all the currently known termination checker algorithms that actually come up with useful results (with the exception of "run until a timeout is hit, say it might not terminate if the timeout is hit, or it does terminate if the timeout is not hit"), you're looking at a few seconds at most. The pain is not the time that the algorithms we know of take, it's the fact that most of them return "undecided" on programs that humans can tell will terminate.

Ada does this too

Posted Feb 13, 2025 16:06 UTC (Thu) by adobriyan (subscriber, #30858) [Link]

> it works in C as well because I believe TRUE is defined as 1 in the standard?

It works because "_Bool + _Bool" is upcasted to "int + int" first and then true's are implicitly upcasted to 1's.