Is the solution to the problem of ending easier than people think?

Although the general case is insoluble, many people still solve problems that are equivalent enough for everyday use.

In his abstract on computer viruses, he showed how virus scanning is tantamount to a stop problem, but we have an entire industry based on this problem.

I also saw the microsoft terminator project - http://research.microsoft.com/Terminator/

What makes me ask - the problem with stopping is overrated - do I need to worry about the general case?

Will the turing type be completed depending on the time, do the types seem to be a good development?

Or, to look the other way, will we start using unused full languages ​​to take advantage of static analysis?

+5
source share
8 answers

Is stopping problem resolution easier than people think?

I think it is as difficult as people think.

Will the type ripen over time?

Darling, they already are!

do dependent types seem like good development?

Highly.

I think that there may be a rise in non-Turing, but nonetheless provable languages. For some time, SQL has been in this category (this is no longer the case), but it really has not diminished its usefulness. I think that for such systems, of course, there is a place.

+14
source

Wow, this is one confusing question.

-: "" , ", ". , .

: , (- , ), , " , ". , , - , . .

-: Turing " " - , . , , .

: "" - , ", ", , . - , . - .

+9

, , .

, "Halts", " " " ", , "Halt" "Do not ". , , " " , . , , .

+4

, , , , . , . Google " X Y", . (muwahaha), ? , " ".

...

+2

, , , . , ; ++. ++ ? ; , , , .

+2

, , , , . , , ( ) , . , , while false do something ( while false).

, Terminator, , , (, , ), , . ( , ) , , . , .

- , , , . - , , , .

0

, , , : ! , , , ( ), , . , : .

, , . DrPizza: , . , , , , : , , .

Finally, the problems associated with dependent types and sub-recursive languages, although partially related, are really different questions, and I'm not sure that you need to mix them all together.

0
source

All Articles