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

Eric Holk

@theinedibleholk

Jan 11

There's precedent for this in dependently typed languages. They forbid infinite loops because infinite loops let you prove anything (they let you do circular reasoning).

Eric Holk

@theinedibleholk

Jan 11

It turns out a lot of code should halt, but some programs shouldn't (e.g. your pacemaker controller). Having non-termination contexts seems like a good way to support both cases well in the same language.

Replying to

and

I'm not really an expert in this, but I think in dependently typed programming you can often check for termination, but you can also check for productivity. Checking for productivity as opposed to termination is useful for building programs that continue indefinitely.

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

Replying to

By 'indefinitely' I mean, so long as you keep providing 'fuel'.