5 ms·

This author predicts that we'll drift towards languages like Agda or Idris, and also discusses how type systems came out of math. I'm curious about two related

by abeppu 7y ago

This author predicts that we'll drift towards languages like Agda or Idris, and also discusses how type systems came out of math. I'm curious about two related questions: 1. Why is it that a minority of math is done with proof systems (i.e. yielding automatically checkable artifacts)? It's burdensome to formalize much of the math that we're interested, even when we're confident in that math. What's the nature of that burden, and how could tools improve to lessen it? 2. Are the difficulties which prevent a lot of math from being done with these systems the same as the difficulties which prevent programmers from using them? There are many invariants that we can easily know about a program, but representing the lot of them in types would be onerous. How do we make that easier/lighter?

zozbot234 7y ago
> Why is it that a minority of math is done with proof systems (i.e. yielding automatically checkable artifacts)? Because most interesting math depends on a lot of other math, and formalizing all of these pre-requirements is a significant burden. The math subfields where this is less of a problem (so-called 'synthetic' mathematics) are also where formalization is being used the most.
- Smaug123 7y ago
  And additionally it takes a lot of effort to formalise a proof. (I say this as someone who has spent nearly two years formalising basic maths in Agda.) It's true in maths as in programming: 90% of the work is in the last 10%, and if you don't get the last 10%, you haven't got a proof.
  - zozbot234 7y ago
    The usual rule of thumb is that 1 page of paper proof leads to 4 pages of "proper" formal proof. Though this may vary depending on how capable the proof assistant is - AIUI, Agda requires you to write out complete proof terms, whereas other systems may be more capable. Sometimes you can use a kind of "reflection" that makes many proofs trivial, simply by defining a decision procedure that's proven to be correct in the general case, and having the system perform the appropriate computations. This is how you would deal, e.g. with trivial simplifications in elementary algebra (that can usually be proven to be valid in any ring, field etc.)
    - Smaug123 7y ago
      Correct, Agda has this notion of reflection. The way to do "tactics" in Agda is simply to manipulate expressions, and there's no meta-language in which to do this: it's just Agda all the way down. It's neat, but not easy.
sesuximo 7y ago
I agree that formal verification can create more work to write programs, but you get a lot more time back in debugging and readability
- tsimionescu 7y ago
  That is simply not true empirically. Formal verification of anything above trivial programs takes years for PhD programmers. There has never even existed a large program (say, more than 200k LoC) that has been formally verified. The most complex formally verified programs I know of are the microkernel SeL4 (~9000 lines of code, excluding the proofs/specs) and CompCert, which I'm still trying to figure out the size of.
tunesmith 7y ago
It's sort of like... say you are on a team that has a ton of legacy code, a ton of technical debt, and a ton of new product requirements always coming in. Why doesn't the team work harder on updating the legacy code and reducing the technical debt? Mathematicians like the new stuff. Some people are working on formalizing the old stuff, it's just slow-going.
- lainga 7y ago
  Do you think there is any place in the mathematical ecosystem, as a career, for mathematicians who do what "should be done", and not what they think they'll like to do? For some (faculty? consensus?) direction of "should be done"?
  - zozbot234 7y ago
    Definitely. Formalizing even a fairly trivial and well-known proof is publishable work (unless someone has done that exact proof already, in a comparable system). It tends to reveal all sorts of interesting details that are entirely hidden in the original proof sketch.
dang 7y ago
> Why is it that a minority of math is done with proof systems If you have that question you owe it to yourself to watch Kevin Buzzard's talk on the topic: https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721
- ncmncm 7y ago
  The reason he had to give that talk is that mathematicians, generally, have no interest at all in changing over to rigorous proofs. It is too much like programming, which they would be doing if that was what they wanted. We will need for the current generation to die off, and another population to come up who started out programming and then got interested in maths. Maybe not the next generation, but the one after. But the original author's dream of proven-correct systems will never happen. You can never prove that software is correct; the best that will ever be possible is that it matches the specification, in a certain subset of expressible details. The bugs are most typically in the remaining details, or in the spec. Fewer bugs is fewer bugs, but the only effective way discovered to have fewer bugs is to have less code for bugs to be in. That means more powerful language features for building libraries that may be thoroughly tested, optimized, and, yes, proven to match the spec.
  - tome 7y ago
    > You can never prove that software is correct; the best that will ever be possible is that it matches the specification That's a bit like saying "You can never prove a mathematical result; the best that will ever be possible is a derivation of a conclusion from a hypothesis".
    - ncmncm 7y ago
      No: all you can prove in math is that a conclusion follows from your choice of axioms. That's fine for math, but software is always part of a system that usually has to, you know, do something useful. The spec is only ever an approximation to that. So, consistent is great, as long as you don't confuse it with right.

by abeppu 7y ago

zozbot234 7y ago

> Why is it that a minority of math is done with proof systems (i.e. yielding automatically checkable artifacts)? Because most interesting math depends on a lot of other math, and formalizing all of these pre-requirements is a significant burden. The math subfields where this is less of a problem (so-called 'synthetic' mathematics) are also where formalization is being used the most.

Smaug123 7y ago
And additionally it takes a lot of effort to formalise a proof. (I say this as someone who has spent nearly two years formalising basic maths in Agda.) It's true in maths as in programming: 90% of the work is in the last 10%, and if you don't get the last 10%, you haven't got a proof.
- zozbot234 7y ago
  The usual rule of thumb is that 1 page of paper proof leads to 4 pages of "proper" formal proof. Though this may vary depending on how capable the proof assistant is - AIUI, Agda requires you to write out complete proof terms, whereas other systems may be more capable. Sometimes you can use a kind of "reflection" that makes many proofs trivial, simply by defining a decision procedure that's proven to be correct in the general case, and having the system perform the appropriate computations. This is how you would deal, e.g. with trivial simplifications in elementary algebra (that can usually be proven to be valid in any ring, field etc.)
  - Smaug123 7y ago
    Correct, Agda has this notion of reflection. The way to do "tactics" in Agda is simply to manipulate expressions, and there's no meta-language in which to do this: it's just Agda all the way down. It's neat, but not easy.

sesuximo 7y ago

I agree that formal verification can create more work to write programs, but you get a lot more time back in debugging and readability

tsimionescu 7y ago
That is simply not true empirically. Formal verification of anything above trivial programs takes years for PhD programmers. There has never even existed a large program (say, more than 200k LoC) that has been formally verified. The most complex formally verified programs I know of are the microkernel SeL4 (~9000 lines of code, excluding the proofs/specs) and CompCert, which I'm still trying to figure out the size of.

tunesmith 7y ago

It's sort of like... say you are on a team that has a ton of legacy code, a ton of technical debt, and a ton of new product requirements always coming in. Why doesn't the team work harder on updating the legacy code and reducing the technical debt? Mathematicians like the new stuff. Some people are working on formalizing the old stuff, it's just slow-going.

lainga 7y ago
Do you think there is any place in the mathematical ecosystem, as a career, for mathematicians who do what "should be done", and not what they think they'll like to do? For some (faculty? consensus?) direction of "should be done"?
- zozbot234 7y ago
  Definitely. Formalizing even a fairly trivial and well-known proof is publishable work (unless someone has done that exact proof already, in a comparable system). It tends to reveal all sorts of interesting details that are entirely hidden in the original proof sketch.

dang 7y ago

> Why is it that a minority of math is done with proof systems If you have that question you owe it to yourself to watch Kevin Buzzard's talk on the topic: https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721

ncmncm 7y ago
The reason he had to give that talk is that mathematicians, generally, have no interest at all in changing over to rigorous proofs. It is too much like programming, which they would be doing if that was what they wanted. We will need for the current generation to die off, and another population to come up who started out programming and then got interested in maths. Maybe not the next generation, but the one after. But the original author's dream of proven-correct systems will never happen. You can never prove that software is correct; the best that will ever be possible is that it matches the specification, in a certain subset of expressible details. The bugs are most typically in the remaining details, or in the spec. Fewer bugs is fewer bugs, but the only effective way discovered to have fewer bugs is to have less code for bugs to be in. That means more powerful language features for building libraries that may be thoroughly tested, optimized, and, yes, proven to match the spec.
- tome 7y ago
  > You can never prove that software is correct; the best that will ever be possible is that it matches the specification That's a bit like saying "You can never prove a mathematical result; the best that will ever be possible is a derivation of a conclusion from a hypothesis".
  - ncmncm 7y ago
    No: all you can prove in math is that a conclusion follows from your choice of axioms. That's fine for math, but software is always part of a system that usually has to, you know, do something useful. The spec is only ever an approximation to that. So, consistent is great, as long as you don't confuse it with right.