[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-20 22:06, Martin Escardo wrote:
> From my personal point of view, Lean has two defects:
> 
>  * It used to support HoTT/UF and it doesn't anymore.
>  * It is ostensively classical and neglects constructive mathematics.
> 
> I understand that for the vast majority of people this is (seen as) an
> advantage.
> 
> But not for me and the people I tend to work with.
> 
> Otherwise Lean is wonderful.
> 


Is its programming language functional? Lazy?
Is it supported compilation and a fast execution?


>  * It is ostensively classical and neglects constructive mathematics.
> 
> I understand that for the vast majority of people this is (seen as) an
> advantage.


Probably the majority of people keep in mind a bit another thing:
   a possibility to use a non-constructive proof, when failed to provide
   a constructive one.

Does Agda support such a possibility?

There is another point: the majority thinks that in constructive logic a 
proof by
contradiction is never possible. But in fact it is very often possible.

As to me, my doubt about the constructive philosophy is as follows.

We have a simple semidecision procedure F for finding an even natural 
number n > 2
which is not a sum of any two primes.
It is search-through, with checking each current n for this property,
where the check for n is by search-through among primes p < n.
It is a difficult problem to solve whether F terminates (whether the 
searched n exists).

And suppose that we are proving a certain goal G by using the procedure 
F, as follows.
"(1) If such  n  exists (the search F terminates), then prove G in one 
way.
  (2) It such does not exist (the search is infinite), then prove B in 
another way.
  If so, then G is proved.
"
I cannot imagine: what can be wrong in this discourse.
In what way can it be possible the result R different from (1) and (2).
How may it look this R ?
The result of (1) or (2) exists in nature independently on whether we 
have shown
some witness or not.
?

--
SM