I quickly looked at pyre and pytype. I wonder : is there a static analyzer for Python that can check for termination guarantee in small snippets of code?
The idea is to have a "safe" and "unsafe" Python (ala Rust) according to some guarantees. Proving termination of program is hard, but it is doable if dev time is dedicated to it, and algorithms are well chosen.
That way, some core libraries could be rewritten and give stronger guarantees.
The idea is used in https://github.com/google/starlark-go which is a subset of Python. People who are used with Python can use it to write imperative config files, and the files are guaranteed to not mess with sensible stuff
The idea is to have a "safe" and "unsafe" Python (ala Rust) according to some guarantees. Proving termination of program is hard, but it is doable if dev time is dedicated to it, and algorithms are well chosen.
That way, some core libraries could be rewritten and give stronger guarantees.
The idea is used in https://github.com/google/starlark-go which is a subset of Python. People who are used with Python can use it to write imperative config files, and the files are guaranteed to not mess with sensible stuff
edit : some starlark design choices explained : https://github.com/bazelbuild/starlark/blob/master/design.md