Wolfram Kahl wrote:

> In the end, my dreams even include a proof format
> that can be checked by the compiler :-)

Dependent types!  That's all you need.

--

        -- Lennart





Reply via email to