FYI: type secure integration of TCL/tk into Qi

[Mark Tarver]

Qi (www.lambdassociates.org) is an advanced functional language built
on top of Lisp that includes optional static typing. It uses sequent
calculus (see Wikipedia http://en.wikipedia.org/wiki/Sequent_calculus)
as the modus operandus for defining types. You can grab a good
summary of Qi from the following places

1. The FAQ page on the home site ( http://www.lambdassociates.org/faq.htm
)
2. The Whats New page. ( http://www.lambdassociates.org/whatsnew.htm )
3. Wikipedia ( http://en.wikipedia.org/wiki/Qi_(programming_language)
)

I've recently integrated a good chunk of TCL/tk into Qi by
axiomatising the type theory implicit in TCL/tk in executable math'l
logic (via the Qi sequent calculus compiler) and the whist program of
my recent posts was the first significant demo program. It was the
first constructive existence proof of the feasibility of the Qi
approach to a large scale case.

The type theory for a big chunk (about 75%) of tk in Qi takes up a 400
line specification which includes a table. This builds over 200
sequent calculus axioms. which in turn generates 27,000 lines of
Common Lisp. More than 3X the size of Qi itself.

Some figures. The whist program demo program of my previous posts
(http://www.lambdassociates.org/Lib/graphics/whist.jpg for screen
shot)
was 561 LOC in its final form and took 317,411inferences to prove type
secure and load. Total time is 5 seconds in CLisp. SBCL would
probably do it in 1-2 seconds but we don't have a port yet.

You can get the system from the Qi library.

http://www.lambdassociates.org/Lib/libraries.htm

see the section on Graphics.

The download for Qi/tk does not include TCL/tk. Note Qi/tk runs under
CLisp and Windows only for now.

Features include:

* concurrent graphics and top level
* constraint propagation - dataflow architecture for widgets
* type security for a big piece of TCL/tk
* capacity for user defined attributes for widgets

Menus remain to be done. They need to be written in Qi/tk itself.

Thanks to all in this group who contributed indirectly by answering my
technical questions on TCL/tk.

Mark