4 ms·

Yes, sure, and that's how mathlib usually gets developed, project by project and PRing missing background material. I'm one of the mathlib maintainers, and I wa

by kmill 3y ago

Yes, sure, and that's how mathlib usually gets developed, project by project and PRing missing background material. I'm one of the mathlib maintainers, and I wanted to be sure there's acknowledgment here for the years of Boubaki-style work among hundreds of volunteers to build up the mathematics. In a way, now that the paper's been formalized it's time for the really hard work, which is figuring out how to restructure it (and mathlib) so that it can easily support future work. That's writing libraries for you. Where are you getting the idea mathlib is being refactored for constructive proofs? I wouldn't say that's on the road map. In fact, the core Lean developers are uninterested in pursuing supporting this. Since you're here, are you able to say why constructive proofs are interesting to program verification or (T)CS people? I've never heard anyone in TCS even know what constructivity is -- Lean supports their case where you write a program/algorithm and then (with classical logic) prove correctness and other properties. What would constructive logic give them?

kmill 3y ago
I'll mention that the "Lean way" for constructivity is that you write `def`s for constructions. These can depend on classical reasoning for well-typedness if you want (like for being sure a number is in range when indexing an array), but there is a computability checker. In particular, the compiler sees if there is a way to lower the `def` into some simply typed IR, and this IR can be further compiled to C. If you trust the compiler, then you can trust whether it's real construction. (Of course, you can also go and prove a definition evaluates to some value if you don't want to trust the evaluator.)
zozbot234 3y ago
> [W]rite a program/algorithm and then (with classical logic) prove correctness. What would constructive logic give them? Compared to the usual case of writing the "algorithm" (i.e. the construction/decision part) and "proof" separately, it basically offers better structuring and composability. Imagine writing an "algorithm" that itself relies for correctness on non-trivial preconditions, or must maintain some invariants etc. Proving correctness of a complete development that might involve wiring up several of these together is quite possible if you can use constructive proofs, but becomes quite tedious if you have to work with the two facets separately. > Where are you getting the idea mathlib is being refactored for constructive proofs? It's not being refactored for constructive proofs, but proofs that do use classical reasoning are being marked as such in a more fine-grained fashion rather than leaving it as the default for the entire development. Which makes it at least possible to add more constructive content.
- kmill 3y ago
  Yeah, I can imagine that, and I've used sigma types to carry it out (`Subtype`s in particular, or perhaps custom structures). Why does the proof in the sigma type have to be constructive? Certainly this is the road to "dependently typed hell" and it's good to avoid mingling proofs with data if you can, but avoiding the law of the excluded middle doesn't make any of that any easier. This is also a bit of a distraction since what I really mean regarding TCS is that in my experience is that they do not see the proofs themselves as being objects-with-properties. They're perfectly happy with non-constructive reasoning to support constructions. I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves. Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs.
  - zozbot234 3y ago
    > Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs. There's been several commits where general appeals to classical reasoning in some development have been replaced by more fine-grained assumptions of decidability for some objects, or marking uses of classical reasoning in some specific proofs. This has not happened throughout mathlib of course, just in some specific places. But it might still show one way of making the development a bit friendlier to alternate foundations. > ...but avoiding the law of the excluded middle doesn't make any of that any easier. Constructivist developments are not about "avoiding the law of excluded middle". They're more about leveraging the way we already structure mathematical proofs (and mathematical reasoning more generally) to make it easier to understand where simple direct reasoning has in fact been used, and a theorem can thus be said to be useful for such purposes. If all we did was proofs by contradiction and excluded middle, there would be no point to it - but direct proof is actually rather common. > Why does the proof in the sigma type have to be constructive? It doesn't, if the constructibility part has been stated separately (e.g. stating that some property is decidable, or that some object is constructible). That's in fact how one can "write the program/algorithm and the logic separately" in a principled way. > I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves. This paper https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/ https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016... provides a reasonable summary of the relevant arguments. It's notable that a number of mathematicians are doing work that involves, e.g. the internal language of topoi, which pretty much amounts to invoking constructive foundations despite starting from what's otherwise a "classical" setting. That they go to all this trouble to do this certainly suggests that they find that work compelling enough. And indeed, it has practical implications wrt. e.g. alternate foundations for analysis, differential geometry etc.

by kmill 3y ago

kmill 3y ago

I'll mention that the "Lean way" for constructivity is that you write `def`s for constructions. These can depend on classical reasoning for well-typedness if you want (like for being sure a number is in range when indexing an array), but there is a computability checker. In particular, the compiler sees if there is a way to lower the `def` into some simply typed IR, and this IR can be further compiled to C. If you trust the compiler, then you can trust whether it's real construction. (Of course, you can also go and prove a definition evaluates to some value if you don't want to trust the evaluator.)

zozbot234 3y ago

> [W]rite a program/algorithm and then (with classical logic) prove correctness. What would constructive logic give them? Compared to the usual case of writing the "algorithm" (i.e. the construction/decision part) and "proof" separately, it basically offers better structuring and composability. Imagine writing an "algorithm" that itself relies for correctness on non-trivial preconditions, or must maintain some invariants etc. Proving correctness of a complete development that might involve wiring up several of these together is quite possible if you can use constructive proofs, but becomes quite tedious if you have to work with the two facets separately. > Where are you getting the idea mathlib is being refactored for constructive proofs? It's not being refactored for constructive proofs, but proofs that do use classical reasoning are being marked as such in a more fine-grained fashion rather than leaving it as the default for the entire development. Which makes it at least possible to add more constructive content.

kmill 3y ago
Yeah, I can imagine that, and I've used sigma types to carry it out (`Subtype`s in particular, or perhaps custom structures). Why does the proof in the sigma type have to be constructive? Certainly this is the road to "dependently typed hell" and it's good to avoid mingling proofs with data if you can, but avoiding the law of the excluded middle doesn't make any of that any easier. This is also a bit of a distraction since what I really mean regarding TCS is that in my experience is that they do not see the proofs themselves as being objects-with-properties. They're perfectly happy with non-constructive reasoning to support constructions. I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves. Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs.
- zozbot234 3y ago
  > Regarding mathlib, could you say what in particular you're talking about, since it's not ringing a bell, and I follow the changelogs. There's been several commits where general appeals to classical reasoning in some development have been replaced by more fine-grained assumptions of decidability for some objects, or marking uses of classical reasoning in some specific proofs. This has not happened throughout mathlib of course, just in some specific places. But it might still show one way of making the development a bit friendlier to alternate foundations. > ...but avoiding the law of the excluded middle doesn't make any of that any easier. Constructivist developments are not about "avoiding the law of excluded middle". They're more about leveraging the way we already structure mathematical proofs (and mathematical reasoning more generally) to make it easier to understand where simple direct reasoning has in fact been used, and a theorem can thus be said to be useful for such purposes. If all we did was proofs by contradiction and excluded middle, there would be no point to it - but direct proof is actually rather common. > Why does the proof in the sigma type have to be constructive? It doesn't, if the constructibility part has been stated separately (e.g. stating that some property is decidable, or that some object is constructible). That's in fact how one can "write the program/algorithm and the logic separately" in a principled way. > I am looking to be convinced that constructive logic is worth it, but this mathematician hasn't seen anything compelling beyond work on foundations themselves. This paper https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/ https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016... provides a reasonable summary of the relevant arguments. It's notable that a number of mathematicians are doing work that involves, e.g. the internal language of topoi, which pretty much amounts to invoking constructive foundations despite starting from what's otherwise a "classical" setting. That they go to all this trouble to do this certainly suggests that they find that work compelling enough. And indeed, it has practical implications wrt. e.g. alternate foundations for analysis, differential geometry etc.