4 ms·

Are there any research projects trying to make "proof" programs / languages?

the_benno 6y ago
Yes, this is an extremely active area of research with lots of connections in the broader programming languages and formal methods communities. For the last decade or so, POPL has had a co-located workshop on proof, the programs of which would be a great place to see the current state of the art. Here's last year's: https://popl20.sigplan.org/home/CPP-2020#event-overview https://popl20.sigplan.org/home/CPP-2020#event-overview
Jtsummers 6y ago
Dependently typed languages may fit what you're asking for. See Idris and the book Type-Driven Development with Idris for an example of encoding critical information into the type system. Beyond that, see SPARK where you're limited to a provable subset of the Ada language (the subset has been extended with each version) so you can make assertions and it will attempt to prove (as part of compilation) that the assertions hold. As in, you could have a function that should always return a non-negative integer, but if it does something like (not fluent, so may be wrong but the principle is correct): function Foo(A : Integer; B :integer) return Integer with Post => Foo'Result > 0; function Foo(A : Integer; B : Integer) return Integer is begin return A - B; end Foo; This should fail when the proof checker is run on this program.
- stan_rogers 6y ago
  Combine Spark with Z as a specification language and you can get to "correct by construction". The only problem seems to be a reluctance to actually formulate a spec.
  - Jtsummers 6y ago
    Yep. I've tried to use Z Notation in the past but haven't had much luck (doesn't help that I had no collaborators so was learning on my own). I've often, also, worked on projects that had decent (but massive and all prose) specs. They would've benefited by formalizing at least portions of them. I'm not sure I'd try to use Z Notation at this point, given that there are other systems out there that seem to fill the same niche but with better tooling. Event-B and TLA+ are the two I've explored the most.
nateberkopec 6y ago
Margaret Hamilton, of Apollo fame, designed and still advocates something called the Universal Systems Language: https://en.wikipedia.org/wiki/Universal_Systems_Language https://en.wikipedia.org/wiki/Universal_Systems_Language
wahern 6y ago
https://en.wikipedia.org/wiki/ATS_(programming_language) https://en.wikipedia.org/wiki/ATS_(programming_language)
emmelaich 6y ago
https://sel4.systems/ https://sel4.systems/ > The seL4® Microkernel. Security is no excuse for bad performance. The benchmark for performance. The world's most highly assured OS kernel. Open source & community-supported under the seL4 Foundation.
lolinder 6y ago
Dafny attempts to do something like this for imperative-style languages, using pre- and post-conditions: https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny
205guy 6y ago
I've noticed several articles about Ada and Rust here on HN recently. Summarizing one comment I saw: Ada has a subset that is provable and certified as such, and Rust is close but not provable nor certified.

Yes, this is an extremely active area of research with lots of connections in the broader programming languages and formal methods communities. For the last decade or so, POPL has had a co-located workshop on proof, the programs of which would be a great place to see the current state of the art. Here's last year's: https://popl20.sigplan.org/home/CPP-2020#event-overview https://popl20.sigplan.org/home/CPP-2020#event-overview

Jtsummers 6y ago

Dependently typed languages may fit what you're asking for. See Idris and the book Type-Driven Development with Idris for an example of encoding critical information into the type system. Beyond that, see SPARK where you're limited to a provable subset of the Ada language (the subset has been extended with each version) so you can make assertions and it will attempt to prove (as part of compilation) that the assertions hold. As in, you could have a function that should always return a non-negative integer, but if it does something like (not fluent, so may be wrong but the principle is correct): function Foo(A : Integer; B :integer) return Integer with Post => Foo'Result > 0; function Foo(A : Integer; B : Integer) return Integer is begin return A - B; end Foo; This should fail when the proof checker is run on this program.

stan_rogers 6y ago
Combine Spark with Z as a specification language and you can get to "correct by construction". The only problem seems to be a reluctance to actually formulate a spec.
- Jtsummers 6y ago
  Yep. I've tried to use Z Notation in the past but haven't had much luck (doesn't help that I had no collaborators so was learning on my own). I've often, also, worked on projects that had decent (but massive and all prose) specs. They would've benefited by formalizing at least portions of them. I'm not sure I'd try to use Z Notation at this point, given that there are other systems out there that seem to fill the same niche but with better tooling. Event-B and TLA+ are the two I've explored the most.

nateberkopec 6y ago

Margaret Hamilton, of Apollo fame, designed and still advocates something called the Universal Systems Language: https://en.wikipedia.org/wiki/Universal_Systems_Language https://en.wikipedia.org/wiki/Universal_Systems_Language

wahern 6y ago

https://en.wikipedia.org/wiki/ATS_(programming_language) https://en.wikipedia.org/wiki/ATS_(programming_language)

emmelaich 6y ago

https://sel4.systems/ https://sel4.systems/ > The seL4® Microkernel. Security is no excuse for bad performance. The benchmark for performance. The world's most highly assured OS kernel. Open source & community-supported under the seL4 Foundation.

lolinder 6y ago

Dafny attempts to do something like this for imperative-style languages, using pre- and post-conditions: https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny

205guy 6y ago

I've noticed several articles about Ada and Rust here on HN recently. Summarizing one comment I saw: Ada has a subset that is provable and certified as such, and Rust is close but not provable nor certified.