Thank Amit for the recap. To amplify a couple things:
Gilbert mentioned potentially recruiting some students to work on the project, which sounds great. To do that we need a message and what works for DARPA is not always what works for students. One way to put this is what's the most interesting part of this topic? I'd guess its lifting - inferring intent from code, in a way that's useful. Transpilation is one use case but not the only one. Can we extract a spec from code? I think that would be super useful.
Second, my experience with using ML is that you *really* need to break the problem down into solvable sub-pieces. One can think of this as curricular learning - how do you get better at something? Start with something simple and add complexity as you get better at it. If the challenge is, let's try to infer intent, let's start with some code where that's relatively easy, and add complexity as we go. One reason I suggest openblas is (1) it uses convenience pointers (2) its functional (3) it has a spec for each function in comments.
So it should be relatively simple (lol) to set as an initial subproblem - hoist openblas into a spec, then produce a verus program as output - rust code plus verus spec, that we use verus to prove correct so we don't need test generation. of course if you think the interesting part is elsewhere then maybe that's not a good initial step and if so lets discuss. I think driver transpilation is super useful, but for everyone I talk to about this, I get back that they wouldn't even know where to start.