Thanks, I didn't know about Chapel. It looks like MATLAB-style languages could be transpiled to/from it, which could lead to big performance improvements.

Also I think I mixed up acronyms 2 weeks ago, and meant TLA+ instead of SAT:

https://news.ycombinator.com/item?id=49909056 (What TLA+ can and can't check)