Running several checkers instead of one

Posted Feb 13, 2025 18:31 UTC (Thu) by daroc (editor, #160859)
In reply to: Running several checkers instead of one by Wol
Parent article: Maintainer opinions on Rust-for-Linux

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.