Hacker News new | past | comments | ask | show | jobs | submit login
Nagini: A Static Verifier for Python [pdf] (ethz.ch)
102 points by Klasiaster 8 months ago | hide | past | web | favorite | 40 comments

This is really, really cool. It's on github at https://github.com/marcoeilers/nagini and you can see examples of the syntax here: http://viper.ethz.ch/nagini-examples/

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.

I'm not sure I understand the benefit. We already have type hints, and for more complicated tests, assert. Both can be ignored in production.

EDIT: ok, I get that they provide some additional benefits such as checking for deadlock or memory leaks. Neat.

Assertions, combined with highly granular code coverage (which most [all?] Python coverage libraries can only do at a line level, so this isn't really sufficient), can almost get you to a point where you're confident that all your asserted invariants are true for all inputs.

Statically checking/proving that those invariants will hold, regardless of inputs, is a huge step up in that level of confidence.

Classic, and nicely done.

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.

Abstract copied from the PDF: We present Nagini, an automated, modular verifier for statically-typed, concurrent Python 3 programs, built on the Viper verification infrastructure. Combining established concepts with new ideas, Nagini can verify memory safety, functional properties, termination, deadlock freedom, and input/output behavior. Our experiments show that Nagini is able to verify non-trivial properties of real-world Python code.

What exactly does verifying memory safety mean in Python? What memory-unsafe operations does Python allow?

We use the term "memory safety" very broadly; what we meant was the absence of runtime errors (e.g., out-of-bounds list accesses), uncaught exceptions, concurrent modification, basically anything that would lead the program to crash. Those aren't memory unsafe in the original sense of the word in Python, but they still crash the program.

Additionally, we prove the absence of data races between threads.

I think (maybe) they mean something like:

  x = Foo()
  wait_on_threads(thread1, thread2) # however that works in python?

Wouldn't that be thread safety? I thought memory safety was things like preventing access to uninitialized or freed memory. As far as I know there's no way to do such things in pure Python.

Fun fact:

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."


Which is no doubt the source for the name Nagini in the Harry Potter books (the familiar of the big bad, Lord Voldemort; a magically-enhanced snake.)

We actually named it after the Harry Potter snake :) There was a wiki at some point that stated that Nagini was a hybrid between a Python and a Viper (Viper is the verification framework that we build on), so that's why.

I’m going to get blasted on this but what if all this python static type checking and such is not needed. Python is python. It’s slower than other languages and that’s ok. I fear that too much is being done and slowly the clean syntax of the language is being eroded.

I think there is something compelling about the combination of a shallow initial learning curve and optional elements like static typing that can improve maintainability for more complex projects. The shallow learning curve makes it easy to get started, then once basic familiarity has been established, one can move on to code that isn't as 'clean'.

'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.

THis. I think the type hint system adds so much visual noise it starts to look like perl. When an attempt to build huge (100k+) project with Python failes, it is not because of the duck typing, but simply because Python is not designed for such use cases.

> When an attempt to build huge (100k+) project with Python failes, it is

...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.

For me, past ~3000 lines, I really work best in a statically compiled language. The type-checking allows me to catch most bugs at compile-time.

Same. I LOVE Python, but if I want to take a project particularly far I tend to end up porting it to a static language. (Usually go these days.)

We almost switched to go at my little startup mostly because of gokit but the syntax is so abhorrent at least to me. I am glad we didn’t. I know it’s peobably stupid to make such a choice but programmer happiness for me comes in part to the syntax and cleanliness of the code. Something I didn’t see in Go

What did you end up going with? I like hearing what problems a language is solving well. :)

C# and Dotnet 2.1, the CTO and another senior dev have years of pro experience with it. I am learning the repository method and such, pretty neat stuff. It compiles to native (which I want to play around with in a lambda setting). The stack is dotnetcore 2.1, c#, k8s, etc., on AWS. Pretty boring stack I guess.

I like C#. I spent a year-ish writing a lot of it and it felt like we produced easy to understand and maintain code. I think the MS/Linux divide is probably the biggest reason more people don’t use it.

Yeah it’s got good support on Linux with vscode but without full visual studio it won’t take off.

I’m not the person you’re asking, but C++ has been the language easiest for me to manage larger projects in. Additionally, the focus on duck typing, generics, and containers makes it a natural language to port to from Python.

I like writing C++ just fine, but managing dependencies drove me crazy. Am I missing something there? When I want to do something simple like import an HTTP lib and make some requests it always feels like a hassle and half the time I get some weird linker error.

I effectively use github as a package manager. I place all dependencies as submodules and handle building the ones which need compilation in my Makefile. Most of the time it works, but boost libraries which aren’t header-only are an absolute nightmare, so I avoid those.

Okay I’m glad to hear that I’m not the only one who found complicated boost libraries to be a total mess. I spent a while banging on managing those. Header-only libraries tended to just work for me.

I actually used Boost for a project, but I only needed header files for the subset I was using. I made each of these a submodule as in [0] and was able to benefit from Boost without all the pains of linking.

So before deciding you can’t use it, see if there’s a way to make it header-only.

[0]: https://github.com/dnbaker/frp/tree/master/boost

That can’t be true. YouTube and some parts of Google run code with substantial python code bases and that was likely written in python 2 and without type hints. Sure they’re refactoring and such today but still

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.

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?

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)

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#.

Python’s type hints have nothing to do with speed.

Since the typing module used to be one of the slowest modules in core you paid a performance penalty even if cpython does no care about type annotations (improved in 3.7). So it does have something to do with performance...

There are other implementations and Python supersets that do use type annotations for optimization and I don't see this trend slowing.

Cython, you mean? There's not really a need for type hints to create speed. A tracing JIT can infer type pretty well.

No he means CPython. While the meaning of the annotations are ignored at runtime, the typing library still has to be imported and typing annotations evaluated (as it evaluate that the type annotation has a value of List[int], not to check that the value tagged with the type annotation actually has that value).

As a result, in CPython 3.6 a module that has been type hinted will import slower than one that doesn't.

> Python supersets that do use type annotations for optimization

Such as Cython.

They way these annotations are used is really not part of the language. I prefer to view it machine-checkable documentations. It's more light-weight an higher level than your C/Java type systems.

Hi everyone, I'm the main author of the tool; it's really cool to see that there's some interest in this :) If you have any questions, I'd be happy to answer them.

Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact