4 ms·

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 th

by 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/

by meuk 7y ago

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/