Hacker News Reader

Comment by snarkypixel | Hacker News Reader

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

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.

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.

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.

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

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/ATS_(programming_language)

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.

Dafny attempts to do something like this for imperative-style languages, using pre- and post-conditions:

https://github.com/dafny-lang/dafny

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.

Reply on news.ycombinator.com