Running several checkers instead of one

Posted Feb 14, 2025 15:12 UTC (Fri) by taladar (subscriber, #68407)
In reply to: Running several checkers instead of one by daroc
Parent article: Maintainer opinions on Rust-for-Linux

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.