4 ms·

The reasoning why this exists is in the very first paragraph... > Python’s lack of safety guarantees can be problematic when, as is increasingly the case, it i

The reasoning why this exists is in the very first paragraph... > Python’s lack of safety guarantees can be problematic when, as is increasingly the case, it is used for critical applications with high correctness demands. The Python community has reacted to this trend by integrating type annotations and optional static type checking into the language [20]. However, there is currently virtually no tool support for reasoning about Python programs beyond type safety.

njharman 8y ago
That's the point. Let Python be Python. Don't ruin what Python is by trying to make it be everything / things it is not. > for critical applications with high correctness demands If you have that use case, pick an appropriate tool. There's more than one programming language ya know?
- carlmr 8y ago
  Exactly, for high correctness I like to use F#, which is also reasonably fast (almost C# speed, with a lot of ML goodies). For high correctness & high performance I think Rust is a great choice, although some of the libraries aren't there yet in terms of maturity. So I usually only use Rust for programs with a small scope where I know that everything I need is available. Or make a DLL with a C interface that I can then call from F#.
- Someone 8y ago
  So, your manager says “the data scientists demoed this. Put it into production”. Do you a) pick an appropriate tool and rewrite their code. b) pick an appropriate tool (python type annotations, this verifier), use it to make the python code robust, and deploy the python code in production? Even if doing a) is as easy as doing b) and produces faster, more efficient code, doing a) again will be more expensive than doing b) again when the data scientists update their python code (even if the typed python and the untyped python are in separate repositories, but ideally, the data scientists would continue working with the ‘solidified’ code, adding duct-typed code at will)

njharman 8y ago

That's the point. Let Python be Python. Don't ruin what Python is by trying to make it be everything / things it is not. > for critical applications with high correctness demands If you have that use case, pick an appropriate tool. There's more than one programming language ya know?

carlmr 8y ago
Exactly, for high correctness I like to use F#, which is also reasonably fast (almost C# speed, with a lot of ML goodies). For high correctness & high performance I think Rust is a great choice, although some of the libraries aren't there yet in terms of maturity. So I usually only use Rust for programs with a small scope where I know that everything I need is available. Or make a DLL with a C interface that I can then call from F#.
Someone 8y ago
So, your manager says “the data scientists demoed this. Put it into production”. Do you a) pick an appropriate tool and rewrite their code. b) pick an appropriate tool (python type annotations, this verifier), use it to make the python code robust, and deploy the python code in production? Even if doing a) is as easy as doing b) and produces faster, more efficient code, doing a) again will be more expensive than doing b) again when the data scientists update their python code (even if the typed python and the untyped python are in separate repositories, but ideally, the data scientists would continue working with the ‘solidified’ code, adding duct-typed code at will)