Incremental improvements to Leo will continue.  Indeed, I have just
spent over an hour reorganizing Leo's to-do list, emphasizing items
that will make a real difference to users.  I expect eventually to
complete all the items in leoToDo.txt, with the exception of those
labelled "vague".

>From time to time, however, I have the desire to use Leo to do
something else besides develop Leo itself.  Now is such a time.  I
plan to revisit the leoInspect module.  The idea is to develop a very
fast inference engine based on what might be called local type
induction.

The idea is simple: we programmers mostly understand code locally.  We
don't have to understand very much to determine what a program is
supposed to do.

For example, most instances of vars called "c" in Leo are (or should
be) leoCommands objects.  The induction step simply verifies that *if*
all input vars c, c1, and c2 *are* leoCommands objects, then any
assignments to other c vars (including via return statements) are
*also* leoCommands objects.

In other words, mathematical "proofs" that type induction must be slow
may be valid in a mathematical sense, but they are not valid in an
engineering sense.  The idea is to "cheat" in such a way that
inferences become very fast and easy.  That's actually what we humans
do.  But we need checks to verify that our "intuitions" are correct.
Those checks are lint-like.  If they fail, they will indicate where
our programs (and especially their naming conventions) can be
improved.

That's the idea.  We'll see how leoInspect can be generalized to
support it.

Edward

-- 
You received this message because you are subscribed to the Google Groups 
"leo-editor" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to 
[email protected].
For more options, visit this group at 
http://groups.google.com/group/leo-editor?hl=en.

Reply via email to