We need a book on correct-by-construction programming in #Agda. PLFA and VFPA are both great books but they worry too much about proofs and don't talk enough about how to use indexed data to write better programs!
-
-
I agree with the blogging, quite frankly
@idrislang literate mode@is great for that! -
Perhaps controversially, I'm not sure it is, in that it encourages showing the annotated end result, but not necessarily the interactions, holes and mistakes along the way.
- 2 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.