The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Klaus,


If you want to see decent sized fully-dependent types experiments in 
certified code generation, you are welcome to examine my (somewhat out 
of date) github developments:

https://github.com/jonleivent/mindless-coding-phase2

https://github.com/jonleivent/mindless-coding

The point of these was to experiment with how to make dependent-type 
guided programming easy enough for non prover-experts.

They are based on the use of one somewhat controversial axiom that 
allows the dependent type residue to be more thoroughly erased from the 
certified code than is otherwise possible in Coq.

I abandoned these mostly due to Ltac causing me more pain than I could 
tolerate.  I await Ltac 2's full implementation before considering 
whether or not to re-attempt.

-- Jonathan


On 12/8/18 2:57 PM, Klaus Ostermann wrote:
> Hi Adam,
> > It actually isn't idiomatic to program with subset types in Coq! I
> > recommend avoiding explicit dependently typed programming whenever
> > possible.  There should be a high standard of justification for any
> > explicit dependent types (which are sometimes the right tool for a
> > job).  It tends to be painful to define and reason about such
> > programs.  Experts generally avoid it.
> thanks for your advice. I actually guessed that much by now. However, my
> intention here was to experience and understand the nature of the pain :)
>
> Klaus