4 ms·

Microsoft, and more importantly Microsoft Research, have many, many projects tackling this. Off the top of my head: the P programming language, F*, Dafny, and a

Microsoft, and more importantly Microsoft Research, have many, many projects tackling this. Off the top of my head: the P programming language, F*, Dafny, and a bunch of others (I think the last two are part of something called Project Everest). Microsoft Research is one of the biggest players in this field. A lot of their efforts span multiple departments so you will have to search around.

SkyMarshal 6y ago
Yup, I'm aware they do a lot of work on this, and hired up half the Haskell and PLT researchers in the world, and have a bunch of projects on it scattered across their web properties. And maybe some of it is trickling down into parts of Windows or .NET, like F# and others, but I wish they'd develop an entire ecosystem around it and make stronger push to commercialize it. With all the aforementioned resources MS has at their disposal, by now they should have their own version of SEL4, comprehensive tooling for secure-by-design and correct-by-construction application development, and optionally secure sandboxed containers for backward compatibility with legacy apps. Though ideally MS funds a Manhattan project for rewriting the most popular apps using their SxD and CxC tooling. Singularity was on the right track, but they let it languish and die for some reason, when instead they could be rebuilding an entire secure/correct ecosystem with Singularity as the focal point, and commercializing it with enterprise support, and selling it to governments and large enterprises with significant security concerns. I wonder why this hasn't happened yet. https://en.wikipedia.org/wiki/Secure_by_design https://en.wikipedia.org/wiki/Secure_by_design https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process/correctness-by-construction https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process...
- ampdepolymerase 6y ago
  It is hard to iterate and make changes when your codebase relies on human/machine assisted proofs. Great for airplanes and cars when regulatory approval means iteration is slow. Not so great for consumer software.
  - SkyMarshal 6y ago
    Good point, though I’d suggest most consumer software, at least office apps and similar needed by the government, are mature enough they don’t need rapid iteration. Most new features being added to them these days are optional at best.

SkyMarshal 6y ago

Yup, I'm aware they do a lot of work on this, and hired up half the Haskell and PLT researchers in the world, and have a bunch of projects on it scattered across their web properties. And maybe some of it is trickling down into parts of Windows or .NET, like F# and others, but I wish they'd develop an entire ecosystem around it and make stronger push to commercialize it. With all the aforementioned resources MS has at their disposal, by now they should have their own version of SEL4, comprehensive tooling for secure-by-design and correct-by-construction application development, and optionally secure sandboxed containers for backward compatibility with legacy apps. Though ideally MS funds a Manhattan project for rewriting the most popular apps using their SxD and CxC tooling. Singularity was on the right track, but they let it languish and die for some reason, when instead they could be rebuilding an entire secure/correct ecosystem with Singularity as the focal point, and commercializing it with enterprise support, and selling it to governments and large enterprises with significant security concerns. I wonder why this hasn't happened yet. https://en.wikipedia.org/wiki/Secure_by_design https://en.wikipedia.org/wiki/Secure_by_design https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process/correctness-by-construction https://us-cert.cisa.gov/bsi/articles/knowledge/sdlc-process...

ampdepolymerase 6y ago
It is hard to iterate and make changes when your codebase relies on human/machine assisted proofs. Great for airplanes and cars when regulatory approval means iteration is slow. Not so great for consumer software.
- SkyMarshal 6y ago
  Good point, though I’d suggest most consumer software, at least office apps and similar needed by the government, are mature enough they don’t need rapid iteration. Most new features being added to them these days are optional at best.