1. 2
  1.  

  2. 1

    Great presentation. Far as application, I already thought this might be useful in lightweight, formal methods to spot problems and suggest corrections for failures in Rust’s borrow checkers, separation logic on C programs, proof tactics, and static analysis tooling. For Rust example, the person might try to express a solution in the language that fails the borrow checker. If they can’t understand why, they submit it to the system that attempts to spot where the problem is. The system might start with humans spotting it and restructuring the code to pass borrow checker. Every instance of those will feed into the learning system that might eventually do that on its own. There’s also potential to use automated, equivalence checks/tests between user-submitted code and the AI’s suggestions to help human-in-the-loop decide if it’s worth review before passing onto the other person.

    (@manishearth @steveklabnik what do you think about the deep learning vs borrow checker idea? Are the troubles you two see across the different uses of borrow checker similar looking enough to possibly be worth attempting that project? It would seem effective if humans already have an intuitive sense for structures to avoid or use as machines can probably find those.)

    In hardware, both digital and analog designers seem to use lots of heuristics in how they design things. Certainly could help there. Might be especially useful in analog due to small number of experienced engineers available.

    1. 3

      failures in Rust’s borrow checkers

      There is only one.

      The system might start with humans spotting [the problem] and restructuring the code to pass [the] borrow checker. Every instance of those will feed into the learning system that might eventually do that on its own.

      DWIM was never a good idea. How can you trust a programming system that replaces the program you wrote (however incorrect it might be) with another program that has a completely different meaning? Are you willing to take responsibility for the program the tool wrote? If not, who will? As you know, tools are not sentient, and thus cannot take responsbiility for anything.

      The borrow checker exposes the complexity of writing programs that manipulate ephemeral resources, and of course this causes pain. However, sweeping these problems under the carpet won’t fix anything. There is no way around actually learning to program.

      1. 1

        Are you willing to take responsibility for the program the tool wrote?

        It’s a suggestion that should be checked for equivalence and comprehension by the developer. If it solved the problem, they should learn from it. If this becomes a panacea, they’ll just run into problems constantly. That passing borrow check is a basic requirement of Rust code in production should (theoretically) encourage them to use the support tool as training wheels until they learn to ride on their own. It shouldn’t substitute for that.

        However, with separation logic or some things in proof, it’s clear reading the literature that a lot of trouble is just in weaknesses of the tooling. Better tactics often automatically find what was manual before. If the spec and algorithm were decent, then a good chunk of that is really mundane stuff that should get automated. Still done with human review of specs for errors and a trusted checker so proof tactics can be untrusted.

        1. 4

          It’s a suggestion that should be checked for equivalence

          The tool you propose replaces an illegal program with a legal one. However:

          • Under a typeless (Curry-style) semantics for Rust, an illegal program may have undefined behavior, whereas a legal program definitely does not. So a legal program semantically equivalent to the original illegal one could well not exist.

          • Under a typeful (Church-style) semantics for Rust, an illegal program is not a program to begin with, so a semantically equivalent legal program definitely does not exist.

          So there are no grounds for talking about program equivalences.

          and comprehension by the developer.

          There exist three kinds of programmers:

          • Those who do not understand ownership and borrowing, and hence will not be able to make heads or tails of the suggestion made by the tool you propose. (Assuming that a meaningful suggestion can be made to begin with, which is not always the case, as shown above.)

          • Those who understand how ownership and borrowing work in Rust, and hence don’t need the tool you propose.

          • Those who understand ownership and borrowing, but not how they work in Rust. What they need to learn is how to express what they already understand using Rust’s syntax, and this is relatively easy task, so they probably have little use for the tool you propose as well.

          However, with separation logic or some things in proof, it’s clear reading the literature that a lot of trouble is just in weaknesses of the tooling.

          By far the most important problem is that coming up with a correct program is hard. This cannot be fixed with tooling. Rust is merely a language in which some of the difficulties involved in coming up with a correct program can be expressed and verifiably avoided.