Hi Ian,
The answer to your question depends on what you want to do with the
specifications you write. My guess is that you want to write
algorithms in TLA+/PlusCal, debug the algorithms using the TLC model
checker (or possibly by writing proofs of correctness that you check
with the TLAPS proof system), and then implement those algorithms in
programs (probably in Python with SciPy and NumPy). If this guess is
incorrect, please stop reading now and tell us what you do want to do
with the specifications.
If you're still reading, the answer depends on whether your algorithms
manipulate real numbers (presumably implemented in the programs with
floating-point arithmetic). If they do, then TLA+ is probably not for
you because TLC does not do arithmetic with real numbers. (If you
only want to write proofs the answer is probably the same because
TLAPS does not have good facilities to handle real arithmetic, but
it's not completely out of the question.)
If you've gotten this far, then your algorithms use only integer
arithmetic and things look promising. So, we come to your question
about SciPy and NumPy, about which I know nothing. Wikipedia tells me
that NumPy provides an efficient implementation of dynamic
multi-dimensional arrays. TLA+ (and hence PlusCal) handles "dynamic
multi-dimensional arrays" (which are simply what mathematicians call
functions over a Cartesian product). However, it does not provide
"efficient implementation". Model checking effectively does
exhaustive testing of a small model of the algorithm--for example,
over all arrays with a very small dimension and a small number of
elements. How big "small" is depends on the application.
As for SciPy, it seems to be a mixed bag. Probably none of the things
it offers are already built into TLA+. Some things are obviously not
something TLA+ is good for--like plotting. Anything that involves
mathematical computations can in principle be written in TLA+.
Anything that can be described by a mathematical function is probably
easy to write in a few lines of TLA+. Other things, like symbolic
math, might be too much work to be worth the effort. Again, don't
expect efficiency.
Leslie