ATS example

[NOTtheMessiah]

An example of using refinement types and dependent types to write a padded string in ATS described below:

http://blog.vmchale.com/article/practical-ats

More about ATS: https://en.wikipedia.org/wiki/ATS_(programming_language)

[hwayne]

That example doesn't match the spec, and doesn't formally prove any properties on its output. This looks closer but I don't know enough ATS to evaluate it. Someone with ATS expertise will have to make a PR with their writeup.