3 ms·
Any recent popular languages with similar support for types of Ada? Is such type system being costly to implement the reason not many other languages pick up th
by mayama 6y ago
Any recent popular languages with similar support for types of Ada? Is such type system being costly to implement the reason not many other languages pick up the feature?
- Kototama 6y agoAda is peculiar because the checks for the ranges are done at runtime. This mean you need a small runtime. A lot of languages are inspired by C and C++ and the types are simple in these languages so it could be an explanation. Haskell has `Numeric.Natural` but I don't think you can define an integer constrained to a range. It probably goes beyond what the type system can do (statically). I think it's possible with Dependent Types (in Idris) but this is rather new.
- Lucretia9 6y agoYou only need to go on programming languages or compilers subreddits to see that they only seem to know C or C++, due to the "hey, I made a language and it's based on C(++), only btter." I look and it's basically the same mistakes each time, the for loop, the basic data types, etc.
- xentropy 6y agoRuntime checks are compiler implementation issue rather than language issue itself. With static analysis compiler could eliminate redundant runtime checks. For example, if SPARK (Ada subset) is used and absense of runtime errors can be proved by GNATprove, then runtime check generation can be disabled in Ada compiler.
- Kototama 6y agoThanks for clarification. Which underlying (type) theory is used in GNATprove?
- xentropy 6y agoI don't know details. GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3). https://github.com/AdaCore/spark2014 https://github.com/AdaCore/spark2014