Conversation

Ahahahaha, yessss I love this so much! Rust is at its best when we're ambitious. And thinking of ways we can practically side-step the halting problem (potentially, maybe, many asteriskses) is certainly not lacking in ambition! Post by

@Sunfishcode

: blog.sunfishcode.online/context-brains

Tangent: Pretty colors

Let's think about one more possible context, for fun:

turing_complete - the ability to have loops (or tail recursion, if Rust adds that), that can't be proved to terminate.

The halting problem gets talked about a lot. However, how often does one actually write loop, as opposed to just using for? If we also had a way to assert that iterator implementations don't repeat themselves, a lot of real-world code might be able to be compatible with !turing_complete.

One of the tricky issues for iterators would be linked lists, which would need to be guaranteed to be acyclic. But it's interesting to note that in Rust, creating a circularly linked list actually requires unsafe anyway. So maybe there's something we could do here.

This would also address the "or infloop" case mentioned above, so we could also get dead-

read image description

ALT

Christian Legnitto

@LegNeato

Jan 12

This looks a lot like Koka

Yosh

@yoshuawuyts

Jan 12

That's right! — Koka is one of the languages we're looking closely at in order to inform the design in Rust.

Brendan Zabarauskas

@brendanzab

Jan 12

Oh this is very exciting to hear! Koka has a bunch of really cool stuff in it! I also highly recommend checking out Effekt and Crochet: - effekt-lang.org - crochet.qteati.me/docs/reference

Brendan Zabarauskas

@brendanzab

Jan 12

Wait I think I might have posted this to you before haha 😳

Replying to

Oh wait it might have somebody else… sorry bit fan of effects systems so it all blurs together, haha. Anyway exciting to effects and capabilities being talked about again in the context of Rust!

9:56 AM · Jan 12, 2022Twitter Web App

Likes