Hacker News Reader

Comment by bayesian_horse | Hacker News Reader

Again the question: Why is this useful?

Is this just for programming language research? What kind of projects would you want to use this language for?

The premise of an axiomatized system is that you can "mechanically" check proofs. So you can also invert the question and ask "Why the hell do we still prove things by hand?".

The answer to that is that there are no good tools and no universally accepted common notation that is amendable to automatic proof checking yet. Those are problems that projects like this want to solve.

I applaud the effort really; it's hard work, and people tend to ask more critical questions ("What is it good for?" "Theorem proving is for academics only") than for any other type of program.

I gather you understand the topic, but I'm still left wondering: who is this for, and what will they do with it?

E.g.: Is the hope to make something all mathematicians will eventually use? Is it targeted at a relatively narrow mathematical field? Is the audience instead programmers looking to prove things about algorithms they're working on?

> I gather you understand the topic, but I'm still left wondering: who is this for, and what will they do with it?

'Understand' is a big word. I've played around with Idris (which is a Haskell-like programming language that supports Homotopy type theory as well). I have a grasp of the underlying mathematics but don't really understand the stuff deeply.

Yes, I went on a bit of a rant and totally ignored your (totally reasonable) question. Theorem proving and proof checking are quite niche, both within computer science and mathematics. In computer science, the idea is that you can formally prove the correctness of computer programs to avoid software failures and have very robust programs. In mathematics, the ideal is to have

  1. A universal language for proofs
  2. A database of computer-verified results
  3. Easy verification of new results

It's a mighty interesting topic, and unfortunately, I've also found it quite difficult to get more than a shallow understanding of it.

Really high assurance code. Stuff like sel4 is used for.

An example of real-world verified software is miTLS: https://www.mitls.org/

A shot in the dark: it could perhaps help in automatically optimizing algorithms by proving that the optimized version is equal to an easily written and reasoned about.

I think reasoning about correctness is easier than about optimizations. Even if you account for a simple complexity model (real computers are a lot more complex, because of techniques like branch prediction or memory caching), proving an implementation as optimal is very hard!

It's often really hard to know if an optimization is "correct"- is the same function as the original, unoptimized version. Formal methods helps here by showing they're equivalent, so you can focus on finding good optimizations instead!

I sympathize with you but I always follow develooments in this space because the potential upside is so awesome. Excellent mathematicians are using theorem provers to check their logic, and such a system brought to say the compilation of a realtime OS, or a distributed transactional system could provide a real safety net for preventing logical errors introduced by new code.

I do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems.

The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else.

For most of the cases where formally verifying _code_ is important, "unit tests" aren't enough. If the person who writes the proofs leaves, you hire someone else to write proofs. Otherwise you don't have a business model.

For most of the cases where formally verifying _designs_ is important (most of the industry), formal specification languages are 1) not actually that hard to learn, and 2) exist distinct from the code, so you can throw them all out if you really need to and go back to flying blind.

"The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else. " - That's because we're an immature field. Something like this will eventually have to come out in order to fix the crisis in software.

We're currently the early explorers of a field, mostly composed practices & tips and tricks that we think help but can't be sure. We're like barber-surgeons before it turned into a true profession.

> I do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems.

That's because the field is still in an exploratory and research phase. Unless you're in an industry where correctness is the most important criteria or involved in research into this stuff, your average programmer isn't going to be using any of this. It's still too early, but that doesn't mean it's a waste of time.

I'm not saying it's a waste of time, I want to understand why it's not.

"who's going to maintain this shit when that rock-star theorem guy is gone?"

At this point, I think the rockstar theorem guy would not be working on some proprietary business logic that needs to be maintained wholly in-house. He'd be in charge of more critical infrastructure in widespread use. Kernels, SSL libraries, optimizing compilers; that sort of thing.

As for who should hire him? I'd hope one of the big tech companies would want a project like this.

I don't see it this way at all. It's more like using the compiler to write good unit tests. That's the hope anyway.

I am dont know so much about that field but I "feel" the same. It would be nice if someone who knows that stuff could reply here if this intuition is right or not. Eventually when we reason about our code "as standard" non-math programmers we are doing math & logic & proofs in our minds aren't we? And we capture the edge cases in forms of tests and hope for the best if we thought about and enumerated all the necessary ones.

So eventually if - a language but more importantly - an ecosystem like that will get leverage, every existing ecosystem can slowly fade into that and develop further in this path.

At the end (almost all) programmers are going to write proofs, because this is what works in scale.

Please correct me if I am wrong!

Well, look who’s afraid for their job to be taken by someone else.

I believe we have plenty of examples today of “we can’t fire this employee because a few years ago we made a mistake of that hire and now they are the only ones who know how that pile of shit works”.

At least with theorem provers the transparent knowledge of the broken systems can be formalized.

https://www.quantamagazine.org/titans-of-mathematics-clash-o...

Imagine if this were just a program you could run that returns 'true' or 'false'

In short to give a confidence in correctness of a program that often exceeds that of other techniques (such as testing). More specifically, from the viewpoint of a programmer there's three general ways that a language like this is useful. I'll use examples from this general class of languages (theorem provers) since Arend is still in its infant stages.

1. As a formalized specification language that allows you to engage in a dialog with the computer about what properties are entailed by such a specification. For example there is a team at Amazon that makes use of the language TLA+ to formally specify some AWS systems and use the computer to derive and check insights about those systems. This focus solely on the specification and ignores the code implementing the specification (this can still be extremely useful). This can also be used to verify the correctness of various CS algorithms.

2. As a language that can be used to check an implementation for conformance against a formal specification to provide a high degree of assurance they match. Examples of this include Isabelle for the microkernel seL4 (a recent post on HN) and Coq for the CompCert certified C compiler (apparently used by Airbus in some capacity and some other safety-critical industries).

3. As a language that can be directly used to generate code (or is in fact compiled/interpreted directly) and prove interesting properties about said code. There's a light version of languages like this in the form of languages like SPARK or analyzers on top of SystemVerilog Assertions, but these bear only a passing resemblance to something like Arend. They are, however, in use by essentially every big chip manufacturer and are widely used again in safety-critical industries. There are languages closer to Arend that try to accomplish something similar, such as again Coq and Isabelle (which allow for extraction of a runnable program in addition to being provers), but I'm not aware of high-profile usages of those.

As far as I'm aware currently Arend is capable of doing the first. I'm not sure if it can do the second. I see no indication it can do the third. Crucially all this can be added later, potentially with little to no modification of the language.

The third use case means in theory these languages (Coq, Isabelle, Arend, etc.) could be used to write ordinary programs. In practice few people do because it's very time-consuming, the tooling is subpar, and there isn't much of a community doing this.

Arend is exciting to me because JetBrains could make a huge dent in the problems of tooling and community (see Kotlin). However, it's unlikely that even if JetBrains gave this its full support suddenly we'd have people writing ordinary web services with Arend. But it might just make other projects with high but not critical safety requirements (e.g. stuff like Kubernetes, Kafka, or at least small modules thereof) plausible to either verify or write directly with Arend.

Reply on news.ycombinator.com