Re: What are Simple Types (Was: Proofs as programs)

On 19/12/2024 02:55, Mild Shock wrote:

 > Advent of Logic 2024: Weekend 2
 > [...]
 > The propositional logic can do with
 > *implication only*, and it should be Linear Logic.
 > French logician Jean-Yves Girard is credited
 > [...]
 It says implication only. Just like here, implication
only is sometimes called positive logic:

Yeah, I didn't think to read another million and one messages for pieces of the problem statement.
I find it too particular: you should be giving a requirement/behaviour, such as indeed an "affine intuitionistic propositional logic (that compiles to some functional code)", not imposing details on the implementation.
-Julio