|Page 30 of 800||Search internet|
In principle, all Logiweb programs are extended lambda terms (extended in that they may include true, If-then-else, and quote). Straightforward execution of such programs is very slow. For that reason, the Logiweb compiler does heavy optimization. Measurements indicate that the Logiweb compiler enhances run times by a factor 1,000,000,000, but the figure it not very accurate.
After optimization, the run times of Logiweb programs can compete with programs expressed in other languages.
At the time of writing, the three largest programs expressed in Logiweb are: the Logiweb compiler itself, a general purpose proof checker for verifying proofs expressed in arbitrary formal theories, and a star tracker. The latter was developed for the European Space Agency as an experiment in using literate programming to reduce the cost of Independent Software Verification and Validation (ISVV).
|Page 30 of 800||Search logiweb.eu|