6 ms·

> Is it possible to have a programming language where the compiler does the formal verification? It is possible, but using separate languages (as seL4 does) ha

> Is it possible to have a programming language where the compiler does the formal verification? It is possible, but using separate languages (as seL4 does) has certain benefits. For example: - Kernel developers tend to have C experience. If the OS is writen in C, they have a much larger pool to hire from. - Any such language would have to be acceptable both for the people who develop the OS and for the people who do the verification: I suspect it's not easy to find something that pleases both crowds. - C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler.

MaxBarraclough 7y ago
Formal methods aren't just an academic curiosity, they have been used for real-world OS work. https://en.wikipedia.org/wiki/SLAM_project https://en.wikipedia.org/wiki/SLAM_project > Less mainstream programming languages get better only if you have an expensive in-house team working on the compiler. Not if you defer optimisation to an external (and actively maintained) backend like LLVM. Rust and Zig do this.
- antoinealb 7y ago
  "Better" is not only a compiler backend thing. Things like better static analysis could also matter. I believe some optimisations are also done by the front end but I don't know enough about compiler design to expand on that.
cwzwarich 7y ago
> C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler. Doesn't SeL4 need -O1 codegen to make their extraction from the generated code (and the thus the rest of the formal proof) work out?
- saithound 7y ago
  The 2017 paper [1] says that they "can handle most of seL4 even at optimisation level 2", presumably it got better in the meantime. Also, it's not like code generation is the only advantage of using a well-supported, externally developed compiler. It's just the one I picked as an illustrative example. GCC releases improve code generation, general usability, diagnostic format support, profilers, etc., at a rate that would be hard to match for a niche language, especially without hiring a dedicated compiler development team. [1] https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449... [2] https://gcc.gnu.org/gcc-9/changes.html https://gcc.gnu.org/gcc-9/changes.html
vbezhenar 7y ago
How will it prove that this new optimization does not introduce bugs? It's not like GCC is verified compiler.
- saithound 7y ago
  Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the semantics of the C source directly. See https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449....
  - zingermc 7y ago
    Ah, it appears that is only done for ARM, but not x86. It would be great if x86 were more amenable to FM, or if we had faster formally-specified processors. Can't wait for a RISC-V workstation!
hinkley 7y ago
Probably an Unsolved Problem in computer programming: If you are trying to solve an old problem a new way, is it necessarily true that having a large pool of applicants is an advantage? It could be a liability. On the one hand, there could be more variance in a large pool, so you might find a lot of unconventional thinkers who think like you. On the other hand, large groups have social mores, and so the dogma might be difficult to overcome, like the old "people can write fortran in any language" problem.

MaxBarraclough 7y ago

Formal methods aren't just an academic curiosity, they have been used for real-world OS work. https://en.wikipedia.org/wiki/SLAM_project https://en.wikipedia.org/wiki/SLAM_project > Less mainstream programming languages get better only if you have an expensive in-house team working on the compiler. Not if you defer optimisation to an external (and actively maintained) backend like LLVM. Rust and Zig do this.

antoinealb 7y ago
"Better" is not only a compiler backend thing. Things like better static analysis could also matter. I believe some optimisations are also done by the front end but I don't know enough about compiler design to expand on that.

cwzwarich 7y ago

> C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler. Doesn't SeL4 need -O1 codegen to make their extraction from the generated code (and the thus the rest of the formal proof) work out?

saithound 7y ago
The 2017 paper [1] says that they "can handle most of seL4 even at optimisation level 2", presumably it got better in the meantime. Also, it's not like code generation is the only advantage of using a well-supported, externally developed compiler. It's just the one I picked as an illustrative example. GCC releases improve code generation, general usability, diagnostic format support, profilers, etc., at a rate that would be hard to match for a niche language, especially without hiring a dedicated compiler development team. [1] https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449... [2] https://gcc.gnu.org/gcc-9/changes.html https://gcc.gnu.org/gcc-9/changes.html

vbezhenar 7y ago

How will it prove that this new optimization does not introduce bugs? It's not like GCC is verified compiler.

saithound 7y ago
Great question. They don't have to trust the compiler: after compilation, they use an SMT-based proof process to establish that the resulting binary matches the semantics of the C source directly. See https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf https://ts.data61.csiro.au/publications/nicta_full_text/6449....
- zingermc 7y ago
  Ah, it appears that is only done for ARM, but not x86. It would be great if x86 were more amenable to FM, or if we had faster formally-specified processors. Can't wait for a RISC-V workstation!

hinkley 7y ago

Probably an Unsolved Problem in computer programming: If you are trying to solve an old problem a new way, is it necessarily true that having a large pool of applicants is an advantage? It could be a liability. On the one hand, there could be more variance in a large pool, so you might find a lot of unconventional thinkers who think like you. On the other hand, large groups have social mores, and so the dogma might be difficult to overcome, like the old "people can write fortran in any language" problem.