Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> (hypothetically, bugs aside)

This is the problem. Interesting computing is some impossibly complex (undecidable, in fact) subset of all computing, that you try to get inside of via the practice of software engineering. Turing's theory of computation provides reasoning tools which allow us to bring rigor to the idea that building correct software that does useful things is generally difficult.

> Designing a computing model that only covers what's useful while also making it convenient appears to be a long standing open problem.

Per the above point, depending on how you characterize this goal, it's probably impossible to accomplish.



>Interesting computing is some impossibly complex (undecidable, in fact) subset of all computing...

I totally disagree here. Or at least I totally disagree that it's a resolved question. All of those nasty problems that face some interesting programs don't face programs we actually write. For example, there is a subset of all turing complete programs that halt. The boundary of that subset isn't decidable, but when I'm writing a program that needs to halt, I write a program I know will halt (why are you pushing to prod if you don't know this program will halt?). Expending a ton of proof effort, I could prove that it halts. So I think the stuff we actually build in practical software is really far from the boundary of the nasty stuff.

Suppose I had a programming language that had a termination checker and only allowed programs it can prove will terminate. We know that the termination checker will have to return yes, no, and who knows. It can't just say yes and no without being wrong sometimes, because it's an undecideable problem. Maybe there's some termination checker that can correctly say yes to all the programs we really care about. Since I could prove that my programs terminate, this checker must exist. A language that only allows these programs must not be turing complete.

So there must be some non turing-complete languages that can express all the programs I would push to prod at work. Maybe some of those languages are even worth using.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: