Arvid Lunnemark

Like you think that spec is hard to generate?

But then also... Even if you have the spec? If you have the spec. But how do you map the spec?

No, the spec would be formal.

I see, I see.

Yeah, yeah. I think you can probably also evolve the spec languages to capture some of the things that they don't really capture right now. I don't know. I think it's very exciting.

I think entire code bases is harder, but that is what I would love to have. And I think it should be possible. Because you can even... There's a lot of work recently where you can prove... formally verified down to the hardware. So you formally verify the C code, and then you formally verify through the GCC compiler, and then through the Verilog down to the hardware.

And that's an incredibly big system, but it actually works. And I think big code bases are sort of similar in that they're a multi-layered system. And if you can decompose it and formally verify each part, then I think it should be possible. I think the specification problem is a real problem, but... How do you handle side effects?

I think it feels possible that you could actually prove that a language model is aligned, for example. Or like you can prove that it actually gives the right answer. That's the dream.

Yeah. And then how do you actually do this? Like we have had a lot of contentious dinner discussions of how do you actually train a bug model? But one very popular idea is, you know, it's kind of potentially easy to introduce a bug than actually finding the bug. And so you can train a model to introduce bugs in existing code.

And then you can train a reverse bug model then that can find bugs using this synthetic data. So that's like one example, but yeah, there are lots of ideas for how to do this.

Yeah, it's a controversial idea inside the company. I think it sort of depends on how much you believe in humanity, almost. I think it would be really cool if you spend nothing to try to find a bug, and if it doesn't find a bug, you spend $0. And then if it does find a bug and you click Accept, then it also shows in parentheses $1. And so you spend $1 to accept the bug.

And then, of course, there's the worry like, okay, we spent a lot of computation. Maybe people will just copy-paste. I think that's a worry. And then there is also the worry that introducing money into the product makes it kind of...

you know like it doesn't feel as fun anymore like you have to like think about money and and you all you want to think about is like the code and so maybe it actually makes more sense to separate it out and like you pay some fee like every month and then you get all of these things for free but there could be a tipping component which is not like it yes but it still has that like dollar symbol i think it's fine but i i also see the point where like maybe you don't want to introduce it

AWS is just really, really good. It's really good. Whenever you use an AWS product, you just know that it's going to work. It might be absolute hell to go through the steps to set it up.

because it's just so good it doesn't need the nature of winning i think it's exactly it's just nature they're winning yeah yeah but aws you can always trust like it will always work and if there is a problem it's probably your problem uh yeah okay is there some interesting like challenges to you guys a pretty new startup to get scaling to like to so many people and

I think the most obvious one is just you want to find out where something is happening in your large code base. And you sort of have a fuzzy memory of, okay, I want to find the place where we do X. But you don't exactly know what to search for in a normal text search.

And so you ask a chat, you hit command enter to ask with the codebase chat, and then very often it finds the right place that you were thinking of.

Yeah, we thought about it, and I think it would be cool to do it locally. I think it's just really hard. And one thing to keep in mind is that some of our users use the latest MacBook Pro, but most of our users, like more than 80% of our users, are in Windows machines, and many of them are not very powerful. And so... local models really only works on the latest computers.

And it's also a big overhead to build that in. And so even if we would like to do that, it's currently not something that we are able to focus on. And I think there are some people that do that, and I think that's great. But especially as models get bigger and bigger and you want to do fancier things with like bigger models, it becomes even harder to do it locally.

There's actually an alternative to local models that I am particularly fond of. I think it's still very much in the research stage, but you could imagine to do homomorphic encryption for language model inference. So you encrypt your input on your local machine, then you send that up, and then the server can use loss of computation.