From 0f0e760ebe7483631922be798113ec8c514c292f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 14 Nov 2005 13:25:05 +0000 Subject: [PATCH] Introduction, again.: --- helm/papers/matita/matita.tex | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index 6738aed4a..b5c27f1bf 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -161,7 +161,20 @@ add an authoring interface, and a set of functionalities for the overall management of the library, integrating everything into a single system. {\em Matita} is the result of this effort. - +At first sight, Matita looks as (and partly is) a Coq clone. This is +more the effect of the circumstances of its creation described +above than the result of a deliberate design. In particular, we +(essentially) share the same foundational dialect of Coq (the +Calculus of Inductive Constructions), the same implementative +language (Ocaml), and the same (script based) authoring philosophy. +However, as we shall see, the analogy essentially stops here. + +In a sense; we like to think of Matita as the way Coq would +look like if entirely rerwritten from scratch: just to give an +idea, although Matita currently supports almost all functionalities of +Coq, it links 60000 lins of coaml code, against ... of Coq (and +we are convinced that, starting from scratch againg, we could furtherly +reduce our code in sensible way). \begin{itemize} -- 2.39.2