Nagini: A Static Verifier for Python [pdf]
pm.inf.ethz.ch
pm.inf.ethz.ch
In the same way that Python's (and Flow/Typescript's) typing lets you describe argument and return types with no more effort/characters than typing a comment, this lets you describe invariants and assertions exactly where you normally would with comments, including invariants on each element of a sequence... and instantly get static typing. I believe there's a custom meta_path importer so it will strip out at module load time, making it zero-cost at runtime. It's the type of thing that there's no reason not to use.
It's powered by Viper, and you can see pseudocode of the internal representation it gets transpiled to in Figure 4 here: http://people.inf.ethz.ch/summersa/wiki/lib/exe/fetch.php?me... . Very smart stuff around tracking read/write dependencies on variables in a programmer-friendly way.
EDIT: ok, I get that they provide some additional benefits such as checking for deadlock or memory leaks. Neat.
Statically checking/proving that those invariants will hold, regardless of inputs, is a huge step up in that level of confidence.
They did something right that's rarely done - their verification extensions to Python are Pythonic. They don't use a separate language for invariants and assertions, and they don't put the assertions in comments. The assertions are thus part of the program.
x = Foo()
thread1.do_something_to_foo(x)
thread2.do_something_to_foo(x)
wait_on_threads(thread1, thread2) # however that works in python?
do_something_to_modified_foo(x)Additionally, we prove the absence of data races between threads.
The name, Nagini, derives from the Sanskrit word for "a deity or class of entity or being taking the form of a very great snake, specifically the king cobra, found in the Indian religions of Hinduism, Buddhism and Jainism."
So before deciding you can’t use it, see if there’s a way to make it header-only.
...because the skills of programmers and other employees hired for this were inadequate. That's it.
It's true for everything. It is possible - and it was demonstrated many, many times - that you can develop huge code bases and successful projects in basically every language in existence, including Asm, PERL, PHP, JavaScript, C, Visual Basic, Cobol, Lisp, Fortran, Prolog and so on. Obviously also including Python.
So if your project, in Python, breaks down above some number of LOC, it's, unfortunately, yours, and only yours, responsibility. Your architecture and/or programming skills were simply not up to the task.
Is it easier to write huge projects in some languages than in other? Yes, of course. Is that difference big enough to justify the claim that it didn't work "simply because Python"? No, not at all.
There are other implementations and Python supersets that do use type annotations for optimization and I don't see this trend slowing.
As a result, in CPython 3.6 a module that has been type hinted will import slower than one that doesn't.
Such as Cython.
'Optional' is key there. Don't want to use type checking? You don't have to.
It's a bit like how some video games introduce one skill or gameplay mechanic at a time, which helps keep players from being overwhelmed by new concepts.
> 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.
> 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?
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#.
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)