Hacker News Reader

Comment by zozbot234 | Hacker News Reader

I'm not sure if I would recommend that, given that Lean has less support for constructive math than some existing systems, and constructive math can be very convenient for proving stuff about programs/computations.

View on HN

Thats not true… in Lean you can restrict yourself to constructive math if you want to for some reason. Just that most actual mathematicians don’t.

> 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?

The 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.

Sure, 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?

Yep, 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).

The Howard-Curry correspondence does not help proving

properties of concurrent systems.

Instead, need to use Actor Event induction:

https://papers.ssrn.com/abstract=3418003

Constructivism 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,

Classical 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

Unfortunately, a theoretical embedding doesn't always accomplish the

work of Double Negation Elimination in practice.

Real mathematicians doesn’t care about constructivist. Also, Lean supports working with both. So you can choose what you want to use.

The mathematicians who study topos theory, the 'internal logic' of whatever category etc. are definitely "real" mathematicians, and they have to care about constructive settings because these come up very naturally in that field. Constructivism is not an isolated niche anymore, it interacts with "real" math too.

At least it's easy to use, i can't for the life of me install and set up agda for example.

This is way off topic, but that's funny, because it's the other way around for me: I can install Agda with a `pacman -S agda`, but I'd need to go through the AUR for Lean.

For this reason, I decided to make Agda playable in the browser here: https://agdapad.quasicoherent.io/ Enjoy! :-)

Reply on news.ycombinator.com