Hacker News Reader

All we need now is a proof that the proof program is correct. And a proof that the proof proving program is correct.

Internal consistency is relatively easy to verify. Completeness to some extent as well.

The manual task is to verify all the assumptions.

Exactly :) And a proof that the spec is correct.

But without formal verification both your spec and the implementation may be incorrect.