SebastianFish

I think you have good points about the file signature and key-verification. I was hoping that we could expand the conversation around static analysis of library functionality as some languages offer features to simplify certain kinds of static analysis. For instance, Rust's borrowing semantics are a language feature that make certain memory usage attributes possible to verify statically.

From a run-time perspective, there are lots of instances where untrusted code has to be executed and there are various sandboxing related approaches there (running in a walled off-VM for instance). From a deployment standpoint that doesn't scale if you need to have an actual VMware instance running per package/dependency. My hope is that a language implemented over a virtual machine might be able to achieve similar levels of security with less overhead.

I think the problem this product is trying to solve, making it easier to implement rigorous testing, is an important one. When I talk to junior developers I compare enterprise software development to painting. When you paint a room, most of your time is actually spent taping out all of the edges and boundaries. The verb painting is a misnomer. Similarly, it isn't a fast or easy for devs to see all of the boundary conditions in inherited code bases and write meaningful tests for them.

You mention in the description about testing code for all possible inputs. Are you all actually doing this behind the scenes with an SMT solver? Are you using some other proof assistant (COQ, HOL, etc) to be able to use proof-by-induction techniques and thus manage the path explosion problem?

I tried out an example comparing two multiplication algorithms (see below) and the tool said it couldn't find any issues in about a minute. Curious whether it will scale to larger problem sizes.

// implementation 1 int mult(int x, int y) { return x*y; } // implementation 2 int slow_mult(int x, int y) { int result=0; if(x<0) { for(int i=x; i<0; i++) { result-=y; } } else { for(int i=0; i<x; i++) { result+=y; } } return result; }

I think you are speaking to one of the core tensions in formal methods. The difference between a specification and an implementation can get blurry. Where formal methods get interesting is statically proving properties about the specification. Take a simple example of a sorting algorithm. The two most commonly proved properties of these algorithms are that they 1) return a permutation of the input list (no items removed or duplicated) and 2) that the output of the list follow some sort of ordering.

One way to look at things is to say the permutation and ordering property checkers are the specification and the actual sorting algorithm is the implementation.

To your point about the specifications being Turing complete, some tools will put restrictions on the specifications to make function termination highly likely. COQ for instance requires that recursive functions be "decreasing in their inputs" AKA that subsequent calls to the same function are passed fewer items or elements than the parent.

Testing different methods of development in terms of speed, cost and quality is really hard. The most convincing approach to me would be a single blind experiment to hire two software development teams and have them build to the same set of requirements in two different ways. But then it is hard to know whether you are really comparing the method of software development or the quality of the software teams. So two software teams isn't enough to get a statistically valid inference. You can see that, given software development rates, this could become a very expensive experiment.

Last point. I think that even writing a specification down to the level that it could be implemented using formal methods might be the biggest game changer. Agile stories rarely come even close to covering all of the potential edge cases. If we had a process that required product owners to literally think through all possible failure modes (what systems of formal methods do) and write out how to handle them then the cost of writing specifications would go way up. Per economics, I think we would end-up with simpler specifications which might be its own benefit.

What interests me most about the development of tools like this is how it might go on to influence the evolution of programming languages. The article that was posted on the CompCert verified C-compiler for instance. What if machine learning could make the cost of developing using more programming languages with stronger guarantees (ie rust, coq, etc) easier? Using languages with more internal checks could also help manage risk the the co-pilot gave a buggy/insecure suggestion.