Hacker News new | past | comments | ask | show | jobs | submit login

"You will never find a programming language that frees you from the burden of thinking about bugs" https://xkcd.com/568/



Moreover, the following theorem is easily proved: there cannot exist a useful general-purpose programming language in which all (or even most) programs can be efficiently verified to be correct, either by man or machine[1].

Where "useful general-purpose" means any language with forward branching and some form of looping recursion (even if bounded) -- it does not need to be Turing complete -- and "efficient" means done in time polynomial in the size of the program.

[1]: ... unless PSPACE = P, in which case some small class of languages that are not quite general purpose but useful nonetheless may have this property, because verifying useful finite-state machine languages is PSPACE-complete.


For those interested, the proof for the Turing-complete and nearly-TC (as in total functional programming) cases is the same as the proof of the time hierarchy theorems[1], and for finite-state-machines the proof is based on results showing that verification of a (concise program expressing) finite state machine is PSPACE-complete. Those results are not surprising, as it is easy to see how any problem in computer science can be reduced (efficiently) to verification, so being able to efficiently prove correctness of a language capable of describing algorithms with super-polynomial complexity (this, BTW, only requires the ability to loop/recurse to depth 2) would mean contradiction.

[1]: https://en.wikipedia.org/wiki/Time_hierarchy_theorem




Consider applying for YC's W25 batch! Applications are open till Nov 12.

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

Search: