Every single talk that I saw from @rosa is just fantastic and highly recommended. 🤩

https://rosa.codes/machines2025/

#brightonruby #rubyconference #RubyProgramming #godelianriddle #goedelianriddle #hilbertsprogram #decidability #entscheidungsproblem #brightonruby2025 #turingmachine #smullyan #raymondsmullyan

Look 'Ma' still no Void, ergonomics aside, *I* think this is cool. I am hoping #TYPES2025 will do too!

```
λΠ> Tree.ALL.all {p=GT 3} (\x => (GreaterThan.isGT 3 x)) (Node 6 Leaf (Node 7 Leaf Leaf))
Left (Here (LTESucc (LTESucc (LTESucc LTEZero))))
```

```
λΠ> decEq [Z,(S Z),(S (S Z))] [1,2,3]
Left (HeadNot MoreRight)
λΠ> decEq [Z,(S Z),(S (S Z))] [Z,(S Z),(S (S Z))]
Right (There Zero (There (Succ Zero) (There (Succ (Succ Zero)) Here)))
λΠ>
```

#dependent_types #constructive_negation #decidability #ITP

Huzzah, I fixed my interface issues.

Although I can do the following stuff before I solved the infrastructure so setting this up is easier.

```
λΠ> Positive.decEq Z (S Z)
Left MoreRight
λΠ> Positive.decEqN Z (S Z)
Right MoreRight
λΠ> Positive.decEq (S Z) (S Z)
Right (Succ Zero)
λΠ> Positive.decEqN (S Z) (S Z)
Left (Succ Zero)
```

#dependent_types #decidability #positive #constructive

On the #TuringMachinw:

“The Most Important Machine That Was Never Built”, Quanta (https://www.quantamagazine.org/alan-turings-most-important-machine-was-never-built-20230503/).

#Turing #AlanTuring #Decidability