5 ms·

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?

ganzuul 7y ago
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.
- Labo333 7y ago
  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!
  - hwayne 7y ago
    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!
meuk 7y ago
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.
- wpietri 7y ago
  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?
  - UK-Al05 7y ago
    Really high assurance code. Stuff like sel4 is used for.
  - meuk 7y ago
    > 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.
  - profquail 7y ago
    An example of real-world verified software is miTLS: https://www.mitls.org/ https://www.mitls.org/
wwarner 7y ago
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.
- bayesian_horse 7y ago
  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.
  - wwarner 7y ago
    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.
    - pezo1919 7y ago
      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!
  - UK-Al05 7y ago
    "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.
dwohnitmok 7y ago
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.
empath75 7y ago
https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/ https://www.quantamagazine.org/titans-of-mathematics-clash-o... Imagine if this were just a program you could run that returns 'true' or 'false'

ganzuul 7y ago

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.

Labo333 7y ago
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!
- hwayne 7y ago
  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!

meuk 7y ago

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.

wpietri 7y ago
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?
- UK-Al05 7y ago
  Really high assurance code. Stuff like sel4 is used for.
- meuk 7y ago
  > 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.
- profquail 7y ago
  An example of real-world verified software is miTLS: https://www.mitls.org/ https://www.mitls.org/

wwarner 7y ago

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.

bayesian_horse 7y ago
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.
- wwarner 7y ago
  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.
  - pezo1919 7y ago
    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!
- UK-Al05 7y ago
  "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.

dwohnitmok 7y ago

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.

empath75 7y ago

https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/ https://www.quantamagazine.org/titans-of-mathematics-clash-o... Imagine if this were just a program you could run that returns 'true' or 'false'