[FOM] 187:Grand Unification 2 - saving human lives

Roger Bishop Jones rbj at rbjones.com
Wed Jul 9 01:36:46 EDT 2003

On Wednesday 09 July 2003  2:24 am, Victor Makarov wrote:
> I can not agree that "Harvey continues to "re-invent the
> wheel"". From recent Harvey Friedman's postings on proof
> checking actually follows that his goal is (in particular) to
> design a practical formal mathematical language - the input
> language of his proof-checking system ("an appropriate
> mathematically friendly functional programming language" can
> be a sublanguage of a practical formal athematical language).
> Have we  invented this "wheel" -- that is, a widely accepted
> practical formal mathematical language? Certainly, not yet.

Indeed not. But this is an aspiration (and not a novel one)
not an achievement.

Roger Jones

More information about the FOM mailing list