On Friday, 6 February 2015 at 05:16:56 UTC, Vlad Levenfeld wrote:
On Friday, 6 February 2015 at 05:05:08 UTC, Ola Fosheim Grøstad
wrote:
OT: Have you looked at Ada SPARK 2014 yet? Provides nice and
strong system programming language semantics. With a
verification tool... nice.
http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html
Even more OT: Most of this doc went over my head. Controlled
types, access types? I only grok that its meant for
safety-critical systems. What's this kind of programming
called? And can you recommend any resources for learning about
the subject from square one?
Access types is Ada speak for pointers.
Ada is quite expressive with pointers, as what the developers are
allowed to do with them depends on their declaration.
Outside the ML languages, Ada is probably the only language that
allows for expressing correct programs just by taking care to
define the right type abstractions.
For example no need to check if a variable is inside a specific
range, if the type only allows that range.
Or no need to check for null pointers if they are declared as non
nullable.
It is one of my favourite languages.
