I think you can usefully tackle this problem without too much difficulty. At least, within a langauge like Gleam you can. An effects tracking system can be use

I think you can usefully tackle this problem without too much difficulty. At least, within a langauge like Gleam you can. An effects tracking system can be used to determine things such as use of FFI, `assert`, recursion, and side effects. With these statements like "this function does not crash" is easy, and "this function does not diverge" is also possible, though it will not detect all functions that do not diverge.