News for hackers. Stuff that matters.

A comment on Coming Soon: Machine-Checked Proofs in Everyday Development. Parent comment

Re:Coming Soon: Machine-Checked Proofs in Everyday Development by bsaul on Sunday December 31, 2017 @11:17AM (#16041081)
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).
[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by firethief on Sunday December 31, 2017 @02:23PM (#16042225)
Short answer: no. Long answer: 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.

[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by bsaul on Sunday December 31, 2017 @02:49PM (#16042444)
As 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
[ Parent | on HN ]
Re:Coming Soon: Machine-Checked Proofs in Everyday Development by hackinthebochs on Sunday December 31, 2017 @02:54PM (#16042490)
But 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.
[ Parent | on HN ]