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

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 10 May 2013 13:18:12 +0200, Yannick Duchêne (Hibou57) wrote:

> 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?

Program implements semantics. If you define the semantics using some other
formalism you don't need the program anymore. The problem is that there is
no formalism, or else the formalism is too powerful for being computable.

> 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.

Human intervention is needed to handle the semantics, not because of
multiplicity of implementations. You could choose them randomly.
 
> 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).

It is not axioms. However the axiomatic framework looks somewhat similar in
the sense that rules of logical inference could be compared with the types
algebra. But there is a sufficient difference that applying algebraic
operations in programming is imperative. You never present a ready type in
order to prove it being a result of some algebraic operations (=algebraic
type). Maybe only in academic studies. Rather you apply operations directly
and the result becomes algebraic merely per construction.

> 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).

No, the program semantics is the meaning of what the program does (to the
customer). That lies outside the language. Not to confuse with the language
semantics which describes how to execute the code (to the CPU).

> 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.

I am not familiar with that, but formal methods are always a meta language
relatively to the programming language and its type system, which are the
object language for them. You never mix the two.

> With this kind of formal system, you typically go from a specification and  
> derives a program.

That won't work. If you can derive the program (in the object language) you
don't need the object language anymore. If that indeed works, as it does
with the Assembly language, you move up to the meta language (higher-level
programming language in this case) and forget about silly lower-level
stuff. Regarding specification languages and modeling language I have
serious reservations about them being capable to replace Ada and other
general purpose languages.

> 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”.

I don't see how Ada 2012 makes it more expressive. It did not extend types
algebra in any significant way.

BTW, static checks if have something to do with expressiveness, then by
hampering it. Because it is evident that the more powerful constructs you
have, less you could prove about their outcome. The most notorious example
is goto. The art of language design is to deploy least powerful constructs,
while keeping it useful for programming.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de