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

[Roger Bishop Jones]

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