[matt_kantor]

> The alternative presented is intuitionist logic, which is practically what in the computing world? Where is it used? Or where could or should it be used?

The Curry-Howard correspondence[1] tells us that every function is a proof (in the intuitionistic sense) of the proposition represented by its return type, given the axioms ("context" in the article) represented by its arguments.

This fact is leveraged heavily by proof assistants (as mentioned in the article), but is generally useful in any statically-typed programming language.

[1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[nyrikki]

The Curry-Howard correspondence formal relationship between intuitionistic logic and typed lambda calculus.

Intuitionistic logic doesn’t hold PEM as a priori.

Due to many issues like [0] you actually lose the univalent in HoTT.

That is what allows you to say two programs are equivalent by behavior.

No comment on the OP, but be careful as it is a rabbit hole.

[0] https://ncatlab.org/nlab/show/Diaconescu-Goodman-Myhill+theo...

[ufocia]

Fuzzy logic may be one approximation. Analog processors may be another.

[matt_kantor]

Did you reply to the wrong comment? I don't see how this relates to what I wrote.