Hey, all. I really don't know what to do with a post like this.
I'm being sincere when I say (as I've said on two threads here) that this genre of posts --- "I'm leaving this company I've been very publicly associated with, and here's the new thing I'm doing" --- is deeply cursed. There's no way to say anything interesting without it just stinking like an ad for the new thing.
Obviously, anything at all you say about a commercial project you're working on is easily read as promotional. And you're right, this kind of writing almost always is promotional. But there's a way to do it where at least you're trying to be in conversation with your peers, rather than hitting people over the head with how awesome you think the project is.
But I don't know how to do that in a post like this. I think the only way to read it is as, like, an investor memo. Not my goal, but I don't make the rules.
So my strategy here is just to stay kind of vague, and talk about where I think the world is going, rather than the specific thing we're doing. I can talk your ears off about capability systems, datalog, models driving hardware, virtualization, whatever. Those are fun conversations and I'm very psyched to have them; it's what lights me up about the work we're doing now.
But I don't think it can work here. I didn't submit this post and I didn't upvote it. I wrote it because I didn't want the whole thing I'm leaving Fly.io for to be wrapped up in some dumb Twitter thread.
If you're unsatisfied with the post, I don't blame you, but it's less a bid for the front page of HN than it is an update to my "about me" page. I'd literally rather talk about HN meta, and how to write for HN, than I would about operating systems at this moment. I truly appreciate the interest though.
These are bad-faith arguments toward "What about self modifying software".
Self modifying software has no grounds in reality or predictable behavior. It is an unreasonable expectation that software is magic. You would not fly on a self-modifying airplane. This is not a future i want to live in.
> How can it be proven correct if it's not deterministic?
Depends on domain, but basically all the same lessons we have for software written the old way by humans.
Which, ah, admittedly isn't great.
> Isn't this the halting problem?
No.
1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.
2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
> 1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.
Making your Turing machine non-deterministic doesn't add any power to it in the sense that the halting problem cares about.
> 2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
Even more so: in practice you write software and proof together. Forget about being able to prove anything about arbitrary software that was written with no proof in mind.
> 3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
Proven correct is a much stronger statement than proven to halt eventually. The form usually has to include the latter.
But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
> Even more so: in practice you write software and proof together. Forget about being able to prove anything about arbitrary software that was written with no proof in mind.
Proof can be done on the program the AI outputs, and doesn't need to be done by the AI.
> But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
We can just tell the AI to do that, at this point. Even in training runs, use automated tests (that reject both clearly-unsafe and also hard-to-prove code) to make sure the code it generates is of that subset.
> Proof can be done on the program the AI outputs, and doesn't need to be done by the AI.
In principle, yes. In practice, people have found it extremely challenging to prove anything about programs that weren't explicitly written to be easy to prove things about.
And AIs are better at writing Lean proofs than just about 99.9% or so of people (exact number is made up). So we might as well have the AI write the proof.
> > But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
> We can just tell the AI to do that, at this point.
Yes, of course. That's my point. And the AI can co-write both proofs and programs.
> Even in training runs, use automated tests (that reject both clearly-unsafe and also hard-to-prove code) to make sure the code it generates is of that subset.
You can only realise that subset, by actually writing the proof.
You can think of these automated proofs like a souped up version of eg Rust's or Haskell's type system. You generally don't write a big chunk of Rust code first, and try to work out how to fit it into the type system afterwards. You co-write both.
People sometimes try to retrofit old Python or JavaScript code with types, and that usually has a lot of problems; and these gradual type systems are not nearly as stringent as you need to be for proper proofs.
> You can only realise that subset, by actually writing the proof.
Absolutely. And then trivially reject programs that have too-long (for whatever value you want) proofs, and train (/fine tune) the models with this as a condition.
If a program is safe, but the smallest proof of it being so is 137 million pages, you can likely already reject it as "too hard" after a million pages even if the program in question is a potential replacement for the Linux kernel.
Maybe. I don't actually think you need to reject long proofs explicitly: they mostly reject themselves in the sense that you can't find them in the first place.
tptacek · · focus · HN ↗
I'm being sincere when I say (as I've said on two threads here) that this genre of posts --- "I'm leaving this company I've been very publicly associated with, and here's the new thing I'm doing" --- is deeply cursed. There's no way to say anything interesting without it just stinking like an ad for the new thing.
Obviously, anything at all you say about a commercial project you're working on is easily read as promotional. And you're right, this kind of writing almost always is promotional. But there's a way to do it where at least you're trying to be in conversation with your peers, rather than hitting people over the head with how awesome you think the project is.
But I don't know how to do that in a post like this. I think the only way to read it is as, like, an investor memo. Not my goal, but I don't make the rules.
So my strategy here is just to stay kind of vague, and talk about where I think the world is going, rather than the specific thing we're doing. I can talk your ears off about capability systems, datalog, models driving hardware, virtualization, whatever. Those are fun conversations and I'm very psyched to have them; it's what lights me up about the work we're doing now.
But I don't think it can work here. I didn't submit this post and I didn't upvote it. I wrote it because I didn't want the whole thing I'm leaving Fly.io for to be wrapped up in some dumb Twitter thread.
If you're unsatisfied with the post, I don't blame you, but it's less a bid for the front page of HN than it is an update to my "about me" page. I'd literally rather talk about HN meta, and how to write for HN, than I would about operating systems at this moment. I truly appreciate the interest though.
access97 · · focus · HN ↗
These are bad-faith arguments toward "What about self modifying software".
Self modifying software has no grounds in reality or predictable behavior. It is an unreasonable expectation that software is magic. You would not fly on a self-modifying airplane. This is not a future i want to live in.
No; sorry, no.
eru · · focus · HN ↗
paulryanrogers · · focus · HN ↗
ben_w · · focus · HN ↗
Depends on domain, but basically all the same lessons we have for software written the old way by humans.
Which, ah, admittedly isn't great.
> Isn't this the halting problem?
No.
1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.
2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
eru · · focus · HN ↗
Making your Turing machine non-deterministic doesn't add any power to it in the sense that the halting problem cares about.
> 2. For practical purposes, it's fine to reject things that take too much effort to prove correct.
Even more so: in practice you write software and proof together. Forget about being able to prove anything about arbitrary software that was written with no proof in mind.
> 3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.
Proven correct is a much stronger statement than proven to halt eventually. The form usually has to include the latter.
But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
ben_w · · focus · HN ↗
Proof can be done on the program the AI outputs, and doesn't need to be done by the AI.
> But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
We can just tell the AI to do that, at this point. Even in training runs, use automated tests (that reject both clearly-unsafe and also hard-to-prove code) to make sure the code it generates is of that subset.
eru · · focus · HN ↗
In principle, yes. In practice, people have found it extremely challenging to prove anything about programs that weren't explicitly written to be easy to prove things about.
And AIs are better at writing Lean proofs than just about 99.9% or so of people (exact number is made up). So we might as well have the AI write the proof.
> > But yes, as said before, we only prove software that's specifically co-written to be easy to prove.
> We can just tell the AI to do that, at this point.
Yes, of course. That's my point. And the AI can co-write both proofs and programs.
> Even in training runs, use automated tests (that reject both clearly-unsafe and also hard-to-prove code) to make sure the code it generates is of that subset.
You can only realise that subset, by actually writing the proof.
You can think of these automated proofs like a souped up version of eg Rust's or Haskell's type system. You generally don't write a big chunk of Rust code first, and try to work out how to fit it into the type system afterwards. You co-write both.
People sometimes try to retrofit old Python or JavaScript code with types, and that usually has a lot of problems; and these gradual type systems are not nearly as stringent as you need to be for proper proofs.
ben_w · · focus · HN ↗
Absolutely. And then trivially reject programs that have too-long (for whatever value you want) proofs, and train (/fine tune) the models with this as a condition.
If a program is safe, but the smallest proof of it being so is 137 million pages, you can likely already reject it as "too hard" after a million pages even if the program in question is a potential replacement for the Linux kernel.
eru · · focus · HN ↗