On Sat, Jul 12, 2014 at 7:12 PM, William ML Leslie < [email protected]> wrote:
> Going through Edwin's video lectures on Idris - especially the one on > the implementation (elaboration to a constructive type theory "TT") > really cemented my understanding of constructive dependant type > systems. > > I think that the simplicity of these systems should make them very > easy to teach. I have enough 'reasonably fresh' programmers laying > around that I should start attempting to validate this. > Thanks for that pointer, William, and for your comments on ATS and Agda. I'll have a look at that video. One of the challenges I'm facing is that BitC isn't a project in isolation. There's other stuff riding on it, so it needs to be *done*, and there's a limit to how much energy I can put into options that don't serve needs that are immediately clear here. Dependent types may not make the cut given the urgency of the need. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
