4.7 Type checking

Prev Up Next Page 33 of 800 Search internet

The fundamental programming language of Logiweb is completely untyped. On top of that, eager data contains tags which allow run-time type checking.

On top of that, authors are free to introduce whatever type system they like. Whenever the Logiweb compiler (lgc) has parsed and macro expanded a page, it invokes a testsuite defined on the page. That testsuite can contain arbitrary tests. Among other, if a page contains formal proofs, the associated proof checker is invoked as part of executing the testsuite.

If the author of a Logiweb page wants to type check all or part of the code on the page, the author must implement a type checker and include it in the testsuite.

Logiweb is liberal. If you want compile time type checking, you can get it. If you want others to benefit from your work, you can publish your type checker. The only thing you cannot do is to restrict other Logiweb users from having the same freedom. Other Logiweb users can use your type checker if they like, but you cannot force it upon anybody.

Prev Up Next Page 33 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05