When I started comma.ai, I saw two ways to go about the jobs problem. One, by starting at the bottom. Drivers will be the first rapid job loss. The other is to start at the top. Computer programmers are the last job to be replaced.
But programmers are different in another way too. A driving agent drives, but it is not made out of drivers, it is made out of programs. A programming agent programs, but it is also made out of programs!
Unlike with a driving agent, this will allow us to improve the program by improving the program. At Backspace, we are making the first program capable of reasoning about itself.
Imagine an equality operator for functions. Of course, this operator cannot work all the time, but it can work often enough. Only famous people can find programs that are hard to decide.
How would you show two programs are equal? You are transforming the code into a latent space.
Is there a space where program equality is simple? Find that, and refactoring, testing, and performance become easy.
Backspace is not a company. I'm not sure what the structure will be. I'm currently building the proof of concept.
If you are interested, reach out. We are looking for people with experience with ML, computer proof systems, PL theory, and solid software engineers.
Here is a fun resource to start playing with formal programming languages.
And here is a beautiful picture of a backspace key.
