5 ms·
> constructive math can be very convenient for proving stuff about programs/computations. How? I can see how proving properties of programs is a place where co
by creata 5y ago
> constructive math can be very convenient for proving stuff about programs/computations.
How? I can see how proving properties of programs is a place where constructivism won't get in the way, but do you have an example of where it can be more convenient?
- logicchains 5y agoThe Howard-Curry correspondence only applies if you stick to constructive maths. This means all your proofs are also programs (and computable) for free. E.g. if trying to prove "blah(x) = blaz(x)" for a fixed x, where blah and blaz are both computable predicates, then the proof can be solved easily just by evaluating blah(x) and blaz(x). This can't be done if blah or blaz isn't computable.
- creata 5y agoSure, but isn't it the case that either your predicates are computable, in which case both a "classical" and a "constructive" proof assistant could evaluate them, or they're not, in which case neither could evaluate them?
- logicchains 5y agoYep, but one could express a computable predicate classically (e.g. by unnecessarily invoking the axiom of choice in its definition). Using a constructive proof assistant prevents accidentally doing this, and encourages using constructive definitions where possible. It also encourages using computable mathematical formulations (e.g. computable reals vs classical reals).
- ProfHewitt 5y agoThe Howard-Curry correspondence does not help proving properties of concurrent systems. Instead, need to use Actor Event induction: https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003
- ProfHewitt 5y agoConstructivism is based on intuitionistic logic, which lacks some important logical principles. For example, it lacks the following principles: * excluded middle * double negation elimination The principles can be valuable for proving properties of concurrent systems,
- rssoconnor 5y agoClassical logic can be embedded into Constructive logic through any one of a number of choices of double negation translations. Thus it is Constructive logic that is arguably more expressive. See https://news.ycombinator.com/item?id=26217587 https://news.ycombinator.com/item?id=26217587
- ProfHewitt 5y agoUnfortunately, a theoretical embedding doesn't always accomplish the work of Double Negation Elimination in practice.