[bakhy]

Why always Peano numbers? If it's doable, I'd love to see something like a web server with provable safety guarantees (e.g. eliminating any SQL injection risk), or a concurrent system with the compiler proving there are no races, even though the code is sharing memory. Or just proving that some simple business rules hold. Is stuff like that doable in a dependently typed language?

[ocharles]

We start with Paeno numbers because they are probably the simplest inductive data type that set the scene for how we tend to proves things in dependently typed programming (inductive reasoning). Proving the things you want are probably doable (I can't say for certain, they are vaguely specified which does not fit with formal methods), but significantly more involved. Trying to take the reader from nothing to that in a single blog post or talk is beyond anyone's ability. Generally, this is because dependent types aren't quite ready for mainstream in terms of convenience.

That said, I'd read some of Edwin Brady's research, as he is actively trying to find the intersection of "business programming" and dependent types: https://edwinb.wordpress.com/publications/

[Zalastax]

Yes, it's possible but might require a lot of effort. For example, my thesis was about creating a system where actors send messages to each other and the system guaranteed that you could not send messages with an unexpected type to another actor. Extending that, you could create a system where messaging has to follow an exact protocol, ensuring that there can be no deadlocks. You can read my work here: https://www.dropbox.com/s/lczrcqu2m9p6osv/Master_Thesis.pdf?... and the code is here: https://github.com/Zalastax/singly-typed-actors

[jackweirdy]

It's not Agda, but you may be interested in this article by Foursquare about how they use Scala Phantom Types to ensure MongoDB queries are semantically well formed at compile time:

https://engineering.foursquare.com/going-rogue-part-2-phanto...

[agbell]

You might like this talk [1] about building a better regex library using dependent type style features. It is really great! The regex is parsed at compile time and then can return better typed information about the capture groups to the lib user. There is also this interview I did with the author on it [2]

[1] https://thestrangeloop.com/2017/dependent-types-in-haskell.h...

[2] https://corecursive.com/015-dependant-types-in-haskell-with-...