"hey, can your wife stop"
"I can't prove that one way or the other."

Follow

who the fuck is scraeming "STOP MAKING HALTING PROBLEM JOKES" at my house. show yourself, coward. it's impossible to prove whether I'll ever stop

one of these days, I'll write up a thing on the halting problem so everyone can laugh with me

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Epilogues:

- Obviously, we can determine if some programs halt, by human analysis or programs that look for certain patterns, but it's impossible to do it for every program.

- This is why you'll see folks use programming languages like Coq and MISRA C that are specifically not Turing complete, and in fact can be proven to halt within a certain amount of time. This sort of thing is used for hard real time applications like air traffic control towers where you absolutely have to do the thing in 50 milliseconds or the plane crashes.

- Your computer isn't exactly a Turing machine because it has finite memory, but close enough.

also, don't feel bad if this doesn't click right away. I didn't get this until three months into a college course on the subject, taught by people who are much more gifted teachers than I am.

You may find it helpful to start with Finite State Machines (also known as Finite State Automata), which are abstract machines like Turing machines, but are a lot less powerful and easier to understand. Most classes start with these and work their way up the Chomsky Hierarchy so you understand why some machines are more powerful than others, what that really means, and why all this talk of accepting and rejecting strings matters.

@BestGirlGrace hahaha I wrote and deleted a response about completely failing to grasp this because I didn't want you to think your writing was the problem. Glad to see that won't happen

@robotcarsley Yeah, I get it. I hope that I can at least contribute to people's understanding, be available to answer questions, and provide things to research if you're interested, but this is absolutely the type of thing best taught with a blackboard and three hours a week.

@BestGirlGrace I didn’t “get” the proof until several months ago, which is to say over three years after I got my CS degree 😶

@vy The proof of the halting problem isn't so bad, but it requires a lot of scaffolding before it really means anything. That's the annoying part.

@BestGirlGrace
I*think* Idris is among those languages, being dependently typed, but I might just be confusing that property for "can check array bound indexing errors at compile time"

Anyway, it's better that we don't use computers as Turing machines, Turing machines are shit to work with as an abstraction.

Anyway, I hope that I'm not just rambling at a point that's not relevant to your thread here.

@violet Looking it up, I don't see anything about Idris's Turing completeness, but a lot of these proof assistant type languages are either not Turing complete (like Coq) or will only accept programs that it knows halt by making every function total.

Turing machines are useful for reasoning about computability, that's it. Kids these days don't care about their long tapes.

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

re: Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

Grace explains the joke (The halting problem, Turing machines, long, nerd nonsense) 

@BestGirlGrace

you wake up to find your garage door is tagged with "NO ROM BASIC"

Sign in to participate in the conversation
Princess Grace's Space Base Place

Don't let the name fool you. All the pornography here is legal, and much of it is hand-written. No fascists, no bigots.