Helyességbizonyítás
A nyelv nem támogatja a helyességbizonyítást.
Valami ellenõrzés azért mégis van. A típusdefiníció mint láttuk tulajdonképpen egy speciális függvénydeklaráció, ami egy tetszõleges értékhez egy logikai értéket rendel. Ez a logikai érték azt jelzi, hogy az ellenõrzött tetszõleges érték eleme-e a típusnak, így igazából egy típusinvariánst kell megfogalmaznunk.
Ha a típustól további típust származtatunk, akkor az új invariáns csak szigoríthatja a régit, mert a régi invariánst is ellenõrzi a rendszer még mielõtt az új invariáns kódja lefutná. A rendszer eleganciáját jelzi hogy ehhez nem vezettek be egy újabb szabályt, mert következik az "értékadáskor ellenõrzünk" szabályból. Az új invariáns egyetlen paramétere õstípus típusúnak van deklarálva és érékadás is történik, tehát lefut az õstípus ellenõrzése, mielõtt a gyermektípusé lefutna.
Írhatunk továbbá assert() jellegû függvényeket, amik
paraméterük igazságértékétõl függõen futásidejû hibát okoznak, vagy
nem csinálnak semmit.
Érdekes lenne a sympel csomagot kibõvíteni öröklõdõ
elõ/utófeltételekkel, és osztályinvariánsokkal.