chotu

3 ms·

1. 1.▲
   by chotu 13y ago

   In ATS2 you can do like this : fun foo {n : int | n > 2} (x : int (n)) : void = println! (x) now calling foo (10) will type check but foo (2) or foo (1) will not.
2. 2.▲
   by chotu 13y ago

   There seem to be misconception that safe language implies inefficient and slow code . It is not so in ATS2 , generated code is quite efficient and is safe even when manipulating memory from ATS2 .
3. 3.▲
   by chotu 13y ago

   You can do specification as type in ATS2 too. My biased view is that I find ATS2 to be far more practical than using coq.