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

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

Le Fri, 10 May 2013 14:40:00 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
>>> 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.
>
> You can't choose randomly, the program must have runtime properties as  
> well.

I should have given another example, a more obvious one: as the program  
derivation is a consequence of a proof the specification is satisfiable  
(the proof and the program are the same thing), automated program  
generation from the specification, would implies automated proof. This  
does not exist with the actual technology, if not for trivial stuffs. So  
far you have proof assistants, not automated provers (just some steps of  
proofs may be automated, if the user request some help from the assistant…  
but it may fail and it's not usable for program generation as far as I  
know).

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