3 ms·
That part made me wonder if a day will come where some generic script would be able to work with any theorem on any code, maybe with the help of some kind of in
by bsaul 9y ago
That part made me wonder if a day will come where some generic script would be able to work with any theorem on any code, maybe with the help of some kind of introspection ( at this level of abstraction i’m not even sure introspection is the right concept).
- deleted 9y ago[deleted]
- firethief 9y agoShort answer: no. Long answer: https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_... There cannot be a program that can prove (or even help a human to prove) any true statement about programs written in a Turing-complete language.
- bsaul 9y agoAs always with this theorem it's pretty hard to be sure if the kind of non provable statement happen often enough to be a concern in practice
- hackinthebochs 9y agoBut most code isn't using the features that make Turing complete languages messy, i.e. evolving the executable code as executing progresses. Most real-world code exists in a subset of Turing complete languages where generic theorem proving could probably work.