4 ms·

If DARPA succeeds in this, it will be a HUGE advantage for everyone. The way I personally see this happening is everything has to be formally verified. This w

If DARPA succeeds in this, it will be a HUGE advantage for everyone. The way I personally see this happening is everything has to be formally verified. This will guarantee that the file written tomorrow will be successfully read by yesterday's programs, and that contemporary software is compatible with future OSes. (Does this mean that we freeze libc?) But there is a problem: there are a lot of quirks for hardware in modern OS/drivers, which add weird and possibly unreliable code. Does the hardware+firmware has to be formally verified too? Do we have to run our software on all hardware that exists, e.g. starting from 6502 and until some future CPU? Do we want to use POSIX? Subset of POSIX? cough Plan9? cough Another problem I see is seemingly inevitable software bloating over time. - What features do we have to include in our OS, our kernel? - Does this list of features only grows over time? - Do we want to have GUI as a requirement? What if UI paradigm changes? There is also a bloating of protocols, e.g. TLS. Maybe replace TLS with CurveCP? Related reading: DOD Trusted Computer System Evaluation Criteria http://csrc.nist.gov/publications/history/dod85.pdf http://csrc.nist.gov/publications/history/dod85.pdf Formally proven OS kernel: http://sel4.systems/ http://sel4.systems/ List of theorem proving systems on wikipedia: http://en.wikipedia.org/wiki/Category:Theorem_proving_software_systems http://en.wikipedia.org/wiki/Category:Theorem_proving_softwa... Note that Nqthm prover started in 1970. ACL2 has a HUGE collection of proofs for code https://github.com/acl2/acl2 https://github.com/acl2/acl2 Jonathan K. Millen, Security Kernel validation in practice (1976), "The correctness of a security kernel on a PDP-11/45 is being proved" DOI:10.1145/360051.360059 https://mega.co.nz/#!U8UAWLQY!YJ1YsOqe6E0jge5lGktBZiJUar1lu2L74JguUoGjP30 https://mega.co.nz/#!U8UAWLQY!YJ1YsOqe6E0jge5lGktBZiJUar1lu2...

ingenter 11y ago
Another relevant question I like to think about: If aliens invented computers, what kind of programming language would they have? What kind of design decisions would they make? My take on the answer is that they would have at least machine codes, some sort of C, some sort of LISP and lambda calculus.
- waterlesscloud 11y ago
  Related, from the last YC RFS about programming tools- "One way to think about this is: what comes after programming languages?" https://www.ycombinator.com/rfs/ https://www.ycombinator.com/rfs/
  - digitalzombie 11y ago
    Algorithms that code themselves I guess. Here's what I want, make it happen. That's an abstraction above programming imo.
- wmf 11y ago
  Urbit? No wait, that's what kind of language alien trolls would have.
  - FractalNerve 11y ago
    related: http://doc.urbit.org/ http://doc.urbit.org/
- vezzy-fnord 11y ago
  Some dialect of APL. It's not that far detached from Lisp, anyway.
CHY872 11y ago
Sounds unpleasant. There are loads of ways of maintaining this property without resorting to formal verification. Hardware is already largely verified, thankfully, and where formally verified software exists it is probably good to use, but in general? You wouldn't have to worry about code bloat for sure; it'd take weeks to write every line of code! The problem is that this sort of code has to be writable by exclusively average developers, and proof assistants just aren't at that level yet (and might never be). A verified implementation of the register colouring algorithm (100 lines of C, perhaps) takes 10,000 lines of code. Useful, yes, but not practical, especially for a whole OS.

ingenter 11y ago

Another relevant question I like to think about: If aliens invented computers, what kind of programming language would they have? What kind of design decisions would they make? My take on the answer is that they would have at least machine codes, some sort of C, some sort of LISP and lambda calculus.

waterlesscloud 11y ago
Related, from the last YC RFS about programming tools- "One way to think about this is: what comes after programming languages?" https://www.ycombinator.com/rfs/ https://www.ycombinator.com/rfs/
- digitalzombie 11y ago
  Algorithms that code themselves I guess. Here's what I want, make it happen. That's an abstraction above programming imo.
wmf 11y ago
Urbit? No wait, that's what kind of language alien trolls would have.
- FractalNerve 11y ago
  related: http://doc.urbit.org/ http://doc.urbit.org/
vezzy-fnord 11y ago
Some dialect of APL. It's not that far detached from Lisp, anyway.

CHY872 11y ago

Sounds unpleasant. There are loads of ways of maintaining this property without resorting to formal verification. Hardware is already largely verified, thankfully, and where formally verified software exists it is probably good to use, but in general? You wouldn't have to worry about code bloat for sure; it'd take weeks to write every line of code! The problem is that this sort of code has to be writable by exclusively average developers, and proof assistants just aren't at that level yet (and might never be). A verified implementation of the register colouring algorithm (100 lines of C, perhaps) takes 10,000 lines of code. Useful, yes, but not practical, especially for a whole OS.