Re: Seeking for papers about tagged types vs access to subprograms

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:

> On Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> I tried to express each validity condition with types and then type  
>> checking.
>
> You cannot express program semantics in terms of types.
>
> If you could express semantics, you won't need to program it.

I don't understand what means “if you could express semantics, you won't  
need to program it”. Or may be you meant the program is already in the  
described semantic? If so, that's indeed be true, as the program can then  
be derived, but there is not a single possible derivation, there are  
typically multiple solutions, so the program still requires human  
intervention to be generated.

Then if you see a types as set of axioms, and an instance of a type, as  
something with which the axioms are all turned into true hypothesis (you  
always need to prove hypothesis are true, before you can infer anything  
which in turn is true, and that must be at the object level for program),  
then you express semantic with types. And types in Ada, already holds  
axioms. Its axiom language is just too limited (ranges and available  
operations, that's near to all what's available).

Then again, semantic is expressed with axioms, or else that's not formal  
semantic, and that's, say, natural language semantic, always subject to  
possible subjective re‑interpretation (no deterministic interpretation).

I will be back to it later and I'm not versed in it enough so far, but  
quickly, Isabelle/HOL (HOL stands for Higher Order Logic here), you have  
something close to that. With Isabelle, axioms and theorems may be  
organized into classes or local theories, which are kind of generic which  
are to be instantiated, this instantiation being named “an interpretation  
of a local theory”. You instantiate providing functions and values as  
arguments.

With this kind of formal system, you typically go from a specification and  
derives a program. Ada do it the other way, and go from the program and  
prove it matches a specification later (either formally proving with SPARK  
or using runtime‑check), or immediately for what is statically checked  
(whether or not an operation exist, whether or not a value belongs to the  
values of a type). But the concept does not imply a direction and would  
make as much sense with the Ada way to go from program and later prove or  
check its properties: in both case, you have to express what is to be  
verified, whatever you do it before you generate a program or after a  
program was authored.

If types could go beyond specification of a simple list of values (and we  
already have a taste of that with discriminated records since always and  
invariant predicates since Ada 2012) and available sub–programs, you won't  
see types as you see it actually, it would look more expressive (and as a  
consequence, safer) and less “rigid”.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University