8 ms·

Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future when we're dealing with increasingly sophisticated AIs. I'm wor

by difc 3mo ago

Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future when we're dealing with increasingly sophisticated AIs. I'm working on similar formal methods but applied to agent sandboxing; do you see Z3 as a better fit than lean? https://github.com/coproduct-opensource/nucleus https://github.com/coproduct-opensource/nucleus

bneb-dev 3mo ago
Salt chose Z3 because it felt right for a compiler. The 100ms timeout means it's not sound, but it's useful. Lean could be the right choice when a proof is a hard requirement?
Taikonerd 3mo ago
> Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future The way I saw this proposed, back in the 2000s: "proof-carrying code."[0] The idea is: the compiler compiles the program, and simultaneously generates a proof that the program doesn't violate X, Y, or Z safety rules. Later, the end-user downloads the program and the proof together, and the local execution environment (the browser, the OS itself, etc) verifies that proof. The idea being: constructing proofs is hard and sometimes involves manual steps. But verifying a proof is easy and automatic. So do the slow, manual thing once, and the fast thing each time the program is downloaded. [0]: https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_code
- luckystarr 3mo ago
  Sounds a bit like Microsoft's Singularity project, though I don't know if they even used a proof system to ensure a program couldn't do bad stuff(TM). After verification they just let the program run in Ring 0 (kernel space) of the CPU to skip even the performance hit of the cpu's isolation.
  - pocksuppet 3mo ago
    I thought Singularity was just building an OS on a memory-safe language and runtime, C# and .NET. The same thing Java tried to do with applets at the browser level.
    - luckystarr 3mo ago
      I listened to an interview with one of the researchers. They had a component to verify "this binary will never allocate mem outside it's allowed area" and by statically verifying that they could enable high performance IPC. Also, that was the source for the decision to allow it to run on Ring 0. That's what stuck in my mind.
      - psd1 3mo ago
        Information is sparse about Singularity, which i understand is the same as Midori. Can you find that interview again? I know about OpenGenera; what left-field OSes might i have missed?
        luckystarr 2mo ago
        Can be that I remembered it incorrectly, as it was in 2008, but here it is: https://se-radio.net/2008/03/episode-88-the-singularity-research-os-with-galen-hunt/ https://se-radio.net/2008/03/episode-88-the-singularity-rese...
        psd1 2mo ago
        Thanks, that was fascinating! I also see that Galen Hunt contributed to Windows Phone, which I adored. (Maybe I'm quixotic, maybe I'm a poor picker, but i love a thing that's beautiful and doomed.)

by difc 3mo ago

bneb-dev 3mo ago

Salt chose Z3 because it felt right for a compiler. The 100ms timeout means it's not sound, but it's useful. Lean could be the right choice when a proof is a hard requirement?

Taikonerd 3mo ago

> Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future The way I saw this proposed, back in the 2000s: "proof-carrying code."[0] The idea is: the compiler compiles the program, and simultaneously generates a proof that the program doesn't violate X, Y, or Z safety rules. Later, the end-user downloads the program and the proof together, and the local execution environment (the browser, the OS itself, etc) verifies that proof. The idea being: constructing proofs is hard and sometimes involves manual steps. But verifying a proof is easy and automatic. So do the slow, manual thing once, and the fast thing each time the program is downloaded. [0]: https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_code

luckystarr 3mo ago
Sounds a bit like Microsoft's Singularity project, though I don't know if they even used a proof system to ensure a program couldn't do bad stuff(TM). After verification they just let the program run in Ring 0 (kernel space) of the CPU to skip even the performance hit of the cpu's isolation.
- pocksuppet 3mo ago
  I thought Singularity was just building an OS on a memory-safe language and runtime, C# and .NET. The same thing Java tried to do with applets at the browser level.
  - luckystarr 3mo ago
    I listened to an interview with one of the researchers. They had a component to verify "this binary will never allocate mem outside it's allowed area" and by statically verifying that they could enable high performance IPC. Also, that was the source for the decision to allow it to run on Ring 0. That's what stuck in my mind.
    - psd1 3mo ago
      Information is sparse about Singularity, which i understand is the same as Midori. Can you find that interview again? I know about OpenGenera; what left-field OSes might i have missed?
      - luckystarr 2mo ago
        Can be that I remembered it incorrectly, as it was in 2008, but here it is: https://se-radio.net/2008/03/episode-88-the-singularity-research-os-with-galen-hunt/ https://se-radio.net/2008/03/episode-88-the-singularity-rese...
        psd1 2mo ago
        Thanks, that was fascinating! I also see that Galen Hunt contributed to Windows Phone, which I adored. (Maybe I'm quixotic, maybe I'm a poor picker, but i love a thing that's beautiful and doomed.)