Fosstodon

alexanderadamEvery single talk that I saw from <a href="https://tu.social/@rosa" class="u-url mention" rel="nofollow noopener" target="_blank">@rosa</a> is just fantastic and highly recommended. 🤩<a href="https://rosa.codes/machines2025/" rel="nofollow noopener" translate="no" target="_blank">https://rosa.codes/machines2025/</a><a href="https://ruby.social/tags/brightonruby" class="mention hashtag" rel="nofollow noopener" target="_blank">#brightonruby</a> <a href="https://ruby.social/tags/rubyconference" class="mention hashtag" rel="nofollow noopener" target="_blank">#rubyconference</a> <a href="https://ruby.social/tags/RubyProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#RubyProgramming</a> <a href="https://ruby.social/tags/godelianriddle" class="mention hashtag" rel="nofollow noopener" target="_blank">#godelianriddle</a> <a href="https://ruby.social/tags/goedelianriddle" class="mention hashtag" rel="nofollow noopener" target="_blank">#goedelianriddle</a> <a href="https://ruby.social/tags/hilbertsprogram" class="mention hashtag" rel="nofollow noopener" target="_blank">#hilbertsprogram</a> <a href="https://ruby.social/tags/decidability" class="mention hashtag" rel="nofollow noopener" target="_blank">#decidability</a> <a href="https://ruby.social/tags/entscheidungsproblem" class="mention hashtag" rel="nofollow noopener" target="_blank">#entscheidungsproblem</a> <a href="https://ruby.social/tags/brightonruby2025" class="mention hashtag" rel="nofollow noopener" target="_blank">#brightonruby2025</a> <a href="https://ruby.social/tags/turingmachine" class="mention hashtag" rel="nofollow noopener" target="_blank">#turingmachine</a> <a href="https://ruby.social/tags/smullyan" class="mention hashtag" rel="nofollow noopener" target="_blank">#smullyan</a> <a href="https://ruby.social/tags/raymondsmullyan" class="mention hashtag" rel="nofollow noopener" target="_blank">#raymondsmullyan</a>

Jan de Muijnck-HughesLook 'Ma' still no Void, ergonomics aside, *I* think this is cool. I am hoping <a href="https://discuss.systems/tags/TYPES2025" class="mention hashtag" rel="nofollow noopener" target="_blank">#TYPES2025</a> 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))) λΠ> ```<a href="https://discuss.systems/tags/dependent_types" class="mention hashtag" rel="nofollow noopener" target="_blank">#dependent_types</a> <a href="https://discuss.systems/tags/constructive_negation" class="mention hashtag" rel="nofollow noopener" target="_blank">#constructive_negation</a> <a href="https://discuss.systems/tags/decidability" class="mention hashtag" rel="nofollow noopener" target="_blank">#decidability</a> <a href="https://discuss.systems/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a>

Jan de Muijnck-HughesHuzzah, 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) ```<a href="https://discuss.systems/tags/dependent_types" class="mention hashtag" rel="nofollow noopener" target="_blank">#dependent_types</a> <a href="https://discuss.systems/tags/decidability" class="mention hashtag" rel="nofollow noopener" target="_blank">#decidability</a> <a href="https://discuss.systems/tags/positive" class="mention hashtag" rel="nofollow noopener" target="_blank">#positive</a> <a href="https://discuss.systems/tags/constructive" class="mention hashtag" rel="nofollow noopener" target="_blank">#constructive</a>

रञ्जित (Ranjit Mathew)On the <a href="https://mastodon.social/tags/TuringMachinw" class="mention hashtag" rel="nofollow noopener" target="_blank">#TuringMachinw</a>:“The Most Important Machine That Was Never Built”, Quanta (<a href="https://www.quantamagazine.org/alan-turings-most-important-machine-was-never-built-20230503/" rel="nofollow noopener" translate="no" target="_blank">https://www.quantamagazine.org/alan-turings-most-important-machine-was-never-built-20230503/</a>).<a href="https://mastodon.social/tags/Turing" class="mention hashtag" rel="nofollow noopener" target="_blank">#Turing</a> <a href="https://mastodon.social/tags/AlanTuring" class="mention hashtag" rel="nofollow noopener" target="_blank">#AlanTuring</a> <a href="https://mastodon.social/tags/Decidability" class="mention hashtag" rel="nofollow noopener" target="_blank">#Decidability</a>

Bornach<a href="https://infosec.exchange/@patrickcmiller" class="u-url mention">@patrickcmiller</a> [Up and Atom] videos on <a href="https://fosstodon.org/tags/computability" class="mention hashtag" rel="tag">#computability</a> <a href="https://youtu.be/t37GQgUPa6k" target="_blank" rel="nofollow noopener" translate="no">https://youtu.be/t37GQgUPa6k</a> <a href="https://youtu.be/PLVCscCY4xI" target="_blank" rel="nofollow noopener" translate="no">https://youtu.be/PLVCscCY4xI</a><a href="https://fosstodon.org/tags/YouTube" class="mention hashtag" rel="tag">#YouTube</a> <a href="https://fosstodon.org/tags/TuringMachines" class="mention hashtag" rel="tag">#TuringMachines</a> <a href="https://fosstodon.org/tags/HaltingProblem" class="mention hashtag" rel="tag">#HaltingProblem</a> <a href="https://fosstodon.org/tags/Decidability" class="mention hashtag" rel="tag">#Decidability</a>

xameer- one can speak unambiguously of the <a href="https://ioc.exchange/tags/decidability" class="mention hashtag" rel="nofollow noopener" target="_blank">#decidability</a> of the word problem for the finitely generated group G.

Recent searches

Search options

Administered by:

Server stats:

#decidability