comp.lang.ada
 help / color / mirror / Atom feed
From: Paul Rubin <no.email@nospam.invalid>
Subject: Re: Ada Distilled by Richard Riehle
Date: Fri, 27 Jul 2018 13:35:19 -0700
Date: 2018-07-27T13:35:19-07:00	[thread overview]
Message-ID: <87muuce7so.fsf@nightsong.com> (raw)
In-Reply-To: 1b5a58b2-65b7-4df8-80b5-03e208d249e1@googlegroups.com

"Dan'l Miller" <optikos@verizon.net> writes:
> Conversely, if Ada'Succ or Ada++ or AdaNG or hypoAda/Ada/hyperAda (or
> whatever its name would be) would embrace overt set operations* over
> the sets of types, subtypes, class-trees, and so forth at either
> compile-time or run-time or both, now that might lead to an
> interesting destination of super-dooper Ada++ doing something special
> & useful that no** other language can do, including current Ada.

Doing those sorts of checks at runtime is not too bad and you can
specify signatures like that for runtime checking with Ruby's contracts
gem.  You can also specify them for the Erlang Dialyzer, which does
static checks but which is intentionally unsound ("success typing").
That is necessary because of Erlang's runtime typing and the body of
existing code that relies on it.  It lets some errors through to avoid
reporting false positives.  I've used both of these and they work,
though Ruby contracts can impose a lot of runtime overhead if you use
them carelessly.  Example: if you have a function whose contract says
its input is an array of widgets, Ruby's contract checker has to scan
the array (which could have a million elements) to make sure that each
element is in fact a widget.

I think for Ada, for that level of precision and given that Ada wants to
be statically checked to the extent possible, you probably want SPARK
rather than stuff in the type system.  You really do need a theorem
prover once the types get that complicated.  But, once you're ok with
that, you can encode anything in types.  That's how Coq works, and
similarly Agda, Idris, etc.  SPARK is probably more in Ada's spirit.

Links:

Ruby contracts: https://github.com/egonSchiele/contracts.ruby
Erlang Dialyzer: http://erlang.org/doc/man/dialyzer.html
Idris example: https://www.idris-lang.org/example/


      parent reply	other threads:[~2018-07-27 20:35 UTC|newest]

Thread overview: 29+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-07-15 18:09 Ada Distilled by Richard Riehle rabbibotton
2018-07-16  1:02 ` Shark8
2018-07-21  6:07   ` Randy Brukardt
2018-07-26  0:42     ` rabbibotton
2018-07-26 20:17       ` Shark8
2018-07-26 21:10         ` Jeffrey R. Carter
2018-07-27  3:01           ` Paul Rubin
2018-07-27 14:32           ` rabbibotton
2018-07-27 20:18             ` Paul Rubin
2018-07-27 17:02           ` Shark8
2018-07-27 14:30         ` rabbibotton
2018-07-27 17:11           ` Shark8
2018-07-27 18:52             ` Dan'l Miller
2018-07-27 20:07               ` Dmitry A. Kazakov
2018-07-27 20:38                 ` Dan'l Miller
2018-07-27 21:32                   ` Dmitry A. Kazakov
2018-07-28  2:41                     ` Dan'l Miller
2018-07-28  7:10                       ` Dmitry A. Kazakov
2018-07-28 15:01                         ` Dan'l Miller
2018-07-28 15:41                           ` Dmitry A. Kazakov
2018-07-28 16:05                             ` Dan'l Miller
2018-08-06 19:33                             ` Vincent
2018-08-06 22:01                               ` Dmitry A. Kazakov
2021-12-09 11:13                                 ` Kevin Chadwick
2018-07-27 21:34                 ` Shark8
2018-07-27 22:16                   ` Dmitry A. Kazakov
2018-07-28  3:52                 ` Dan'l Miller
2018-07-28  7:12                   ` Dmitry A. Kazakov
2018-07-27 20:35               ` Paul Rubin [this message]
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox