search

hwayne / lets-prove-leftpad

Proving leftpad correct two-dozen different ways
Other
651 stars 62 forks source link

ATS example #13

Open NOTtheMessiah opened 6 years ago

NOTtheMessiah commented 6 years ago

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 commented 6 years ago

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.