# Trying Project Euler in ATS

**URL:** <https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253>\
**Category:** Google Group\
**Created:** [January 14, 2015, 12:21am UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253 "2015-01-14T00:21:22Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 14, 2015, 12:21am UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253/1 "2015-01-14T00:21:22Z")

</div>

Here is the link to Project Euler:

[https://projecteuler.net](https://projecteuler.net)

In the past, I found it quite interesting to solve in ATS some of the  
problems published  
at Project Euler. This can also be particularly effective for teaching  
oneself various concepts  
of program verification.

I have just set up the following ATS-project:

> **[githwxi/ATS-Postiats-contrib](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER)**
>
> ATS-Postiats-contrib is primarily for packages contributed to ATS-Postiats - githwxi/ATS-Postiats-contrib

I hope that the ATS community will have a considerably significant amount  
of interest in this  
so that this effort can continue in a meaningful way.

Let me take the first problem ([https://projecteuler.net/problem=1](https://projecteuler.net/problem=1)) as an  
example:

If we list all the natural numbers below 10 that are multiples of 3 or 5,  
we get 3, 5, 6 and 9. The sum of these multiples is 23.

Find the sum of all the multiples of 3 or 5 below 1000.

I give a specification of this problem in the following file:

> <https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats>

This specification has been implemented in the following file:

> <https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats>

In general, a problem can have multiple specifications and each  
specification can have multiple solutions  
(that is, implementations).

I hope that people interested in this will contribute both specifications  
and solutions. As a community, we  
can review them together and likely improve them as well.

At this point, I would like to mostly work as a reviewer/editor. If you  
contribute, please send your code to  
this list or to me directly.

The following link leads to a solution to the first problem that can be  
type-checked using Patsopt-as-a-service  
(Patsoptaas):

[http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats)

The following link leads to a variant of the above solution that can be  
tested (that is, run) using Patsopt-as-a-service:

[http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats)

Cheers!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 16, 2015, 6:55am UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253/2 "2015-01-16T06:55:44Z")

</div>

P1 is not very interesting. P16 is a very good one.  
The specification I gave for P16 is not yet a full specification.

Solving math puzzles in ATS can be a very effective way to learn dependent  
types  
and programming with theorem-proving. It can help one quickly grow familiar  
with type-checking  
and type-error messages.

Doing something “useful” or “realistic” is always very hard at the  
beginning.  
Before one can play Chopin or Brahms, one probably needs to play “Twinkle,  
twinkle, little star” :)On Friday, January 16, 2015 at 1:34:05 AM UTC-5, Brandon Barker wrote:

> This does seem like a good way to learn ATS/LF, but at the risk of  
> sounding obtuse, after staring at the specification of P1 a while, I have  
> to wonder if it would be necessary to write an implementation to prove my  
> specification ;). I think Knuth has an applicable quote here, so it can’t  
> hurt at least. The typechecker can only prove coherency, not that I haven’t  
> proved something else, after all.
> 
> Then again, proving something by accident unintentionally may be rare as  
> well.
> 
> All that said, I guess as is pointed out in the ATS book, you probably get  
> used to these recursive proofs after a while.
> 
> On Wed, Jan 14, 2015 at 11:34 PM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > FYI.
> > 
> > I wrote a README available here:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER)
> > 
> > On Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:
> > 
> > > FYI.
> > > 
> > > Problem 16
> > > 
> > > 2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.
> > > 
> > > What is the sum of the digits of the number 2^1000?
> > > 
> > > Here is the specification for this problem:
> > > 
> > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > master/projects/MEDIUM/PEULER/P16/P16.sats
> > > 
> > > Note that the specification in P16.sats is not yet a “full”  
> > > specification. If there is some interest, we could  
> > > do one later.
> > > 
> > > On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:
> > > 
> > > > FYI.
> > > > 
> > > > Even Fibonacci numbers
> > > > 
> > > > Problem 2
> > > > 
> > > > Each new term in the Fibonacci sequence is generated by adding the  
> > > > previous two terms. By starting with 1 and 2, the first 10 terms will  
> > > > be:
> > > > 
> > > > 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …
> > > > 
> > > > By considering the terms in the Fibonacci sequence whose values do not  
> > > > exceed four million, find the sum of the even-valued terms.
> > > > 
> > > > Here is the specification for the second problem:
> > > > 
> > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > master/projects/MEDIUM/PEULER/P2/P2.sats
> > > > 
> > > > Any solutions/implementations 🙂
> > > > 
> > > > On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:
> > > > 
> > > > > Here is the link to Project Euler:
> > > > > 
> > > > > [https://projecteuler.net](https://projecteuler.net)
> > > > > 
> > > > > In the past, I found it quite interesting to solve in ATS some of the  
> > > > > problems published  
> > > > > at Project Euler. This can also be particularly effective for teaching  
> > > > > oneself various concepts  
> > > > > of program verification.
> > > > > 
> > > > > I have just set up the following ATS-project:
> > > > > 
> > > > > [https://github.com/githwxi/ATS-Postiats-contrib/tree/](https://github.com/githwxi/ATS-Postiats-contrib/tree/)  
> > > > > master/projects/MEDIUM/PEULER
> > > > > 
> > > > > I hope that the ATS community will have a considerably significant  
> > > > > amount of interest in this  
> > > > > so that this effort can continue in a meaningful way.
> > > > > 
> > > > > Let me take the first problem ([#1 Multiples of $3$ or $5$ - Project Euler](https://projecteuler.net/problem=1)) as  
> > > > > an example:
> > > > > 
> > > > > If we list all the natural numbers below 10 that are multiples of 3 or  
> > > > > 5, we get 3, 5, 6 and 9. The sum of these multiples is 23.
> > > > > 
> > > > > Find the sum of all the multiples of 3 or 5 below 1000.
> > > > > 
> > > > > I give a specification of this problem in the following file:  
> > > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > > master/projects/MEDIUM/PEULER/P1/P1.sats
> > > > > 
> > > > > This specification has been implemented in the following file:
> > > > > 
> > > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > > master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats
> > > > > 
> > > > > In general, a problem can have multiple specifications and each  
> > > > > specification can have multiple solutions  
> > > > > (that is, implementations).
> > > > > 
> > > > > I hope that people interested in this will contribute both  
> > > > > specifications and solutions. As a community, we  
> > > > > can review them together and likely improve them as well.
> > > > > 
> > > > > At this point, I would like to mostly work as a reviewer/editor. If  
> > > > > you contribute, please send your code to  
> > > > > this list or to me directly.
> > > > > 
> > > > > The following link leads to a solution to the first problem that can  
> > > > > be type-checked using Patsopt-as-a-service  
> > > > > (Patsoptaas):
> > > > > 
> > > > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_)  
> > > > > serve.php?mycode\_url=[https://raw.githubusercontent.com/](https://raw.githubusercontent.com/)  
> > > > > githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/  
> > > > > P1//P1-hwxi.dats
> > > > > 
> > > > > The following link leads to a variant of the above solution that can  
> > > > > be tested (that is, run) using Patsopt-as-a-service:
> > > > > 
> > > > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_)  
> > > > > serve.php?mycode\_url=[https://raw.githubusercontent.com/](https://raw.githubusercontent.com/)  
> > > > > githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/  
> > > > > P1/JS/P1-hwxi.dats
> > > > > 
> > > > > Cheers!
> > > > > 
> > > > > –  
> > > > > You received this message because you are subscribed to the Google Groups  
> > > > > “ats-lang-users” group.  
> > > > > To unsubscribe from this group and stop receiving emails from it, send an  
> > > > > email to [ats-lang...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > \<javascript:\>.  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > > To view this discussion on the web visit  
> > > > > [https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com)  
> > > > > [https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > .
> 
> –  
> Brandon Barker  
> [brand...@gmail.com](mailto:brand...@gmail.com) \<javascript:\>

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 15, 2015, 4:34am UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253/3 "2015-01-15T04:34:47Z")

</div>

FYI.

I wrote a README available here:

[https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULEROn](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULEROn) Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:

> FYI.
> 
> Problem 16
> 
> 2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.
> 
> What is the sum of the digits of the number 2^1000?
> 
> Here is the specification for this problem:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P16/P16.sats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P16/P16.sats)
> 
> Note that the specification in P16.sats is not yet a “full” specification.  
> If there is some interest, we could  
> do one later.
> 
> On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:
> 
> > FYI.
> > 
> > Even Fibonacci numbers
> > 
> > Problem 2
> > 
> > Each new term in the Fibonacci sequence is generated by adding the  
> > previous two terms. By starting with 1 and 2, the first 10 terms will be:
> > 
> > 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …
> > 
> > By considering the terms in the Fibonacci sequence whose values do not  
> > exceed four million, find the sum of the even-valued terms.
> > 
> > Here is the specification for the second problem:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P2/P2.sats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P2/P2.sats)
> > 
> > Any solutions/implementations 🙂
> > 
> > On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:
> > 
> > > Here is the link to Project Euler:
> > > 
> > > [https://projecteuler.net](https://projecteuler.net)
> > > 
> > > In the past, I found it quite interesting to solve in ATS some of the  
> > > problems published  
> > > at Project Euler. This can also be particularly effective for teaching  
> > > oneself various concepts  
> > > of program verification.
> > > 
> > > I have just set up the following ATS-project:
> > > 
> > > [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER)
> > > 
> > > I hope that the ATS community will have a considerably significant  
> > > amount of interest in this  
> > > so that this effort can continue in a meaningful way.
> > > 
> > > Let me take the first problem ([#1 Multiples of $3$ or $5$ - Project Euler](https://projecteuler.net/problem=1)) as  
> > > an example:
> > > 
> > > If we list all the natural numbers below 10 that are multiples of 3 or 5  
> > > , we get 3, 5, 6 and 9. The sum of these multiples is 23.
> > > 
> > > Find the sum of all the multiples of 3 or 5 below 1000.
> > > 
> > > I give a specification of this problem in the following file:
> > > 
> > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats)
> > > 
> > > This specification has been implemented in the following file:
> > > 
> > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats)
> > > 
> > > In general, a problem can have multiple specifications and each  
> > > specification can have multiple solutions  
> > > (that is, implementations).
> > > 
> > > I hope that people interested in this will contribute both  
> > > specifications and solutions. As a community, we  
> > > can review them together and likely improve them as well.
> > > 
> > > At this point, I would like to mostly work as a reviewer/editor. If you  
> > > contribute, please send your code to  
> > > this list or to me directly.
> > > 
> > > The following link leads to a solution to the first problem that can be  
> > > type-checked using Patsopt-as-a-service  
> > > (Patsoptaas):
> > > 
> > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats)
> > > 
> > > The following link leads to a variant of the above solution that can be  
> > > tested (that is, run) using Patsopt-as-a-service:
> > > 
> > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats)
> > > 
> > > Cheers!

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [January 16, 2015, 6:33am UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253/4 "2015-01-16T06:33:44Z")

</div>

This does seem like a good way to learn ATS/LF, but at the risk of sounding  
obtuse, after staring at the specification of P1 a while, I have to wonder  
if it would be necessary to write an implementation to prove my  
specification ;). I think Knuth has an applicable quote here, so it can’t  
hurt at least. The typechecker can only prove coherency, not that I haven’t  
proved something else, after all.

Then again, proving something by accident unintentionally may be rare as  
well.

All that said, I guess as is pointed out in the ATS book, you probably get  
used to these recursive proofs after a while.On Wed, Jan 14, 2015 at 11:34 PM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> FYI.
> 
> I wrote a README available here:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER)
> 
> On Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:
> 
> > FYI.
> > 
> > Problem 16
> > 
> > 2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.
> > 
> > What is the sum of the digits of the number 2^1000?
> > 
> > Here is the specification for this problem:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > master/projects/MEDIUM/PEULER/P16/P16.sats
> > 
> > Note that the specification in P16.sats is not yet a “full”  
> > specification. If there is some interest, we could  
> > do one later.
> > 
> > On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:
> > 
> > > FYI.
> > > 
> > > Even Fibonacci numbers
> > > 
> > > Problem 2
> > > 
> > > Each new term in the Fibonacci sequence is generated by adding the  
> > > previous two terms. By starting with 1 and 2, the first 10 terms will be  
> > > :
> > > 
> > > 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …
> > > 
> > > By considering the terms in the Fibonacci sequence whose values do not  
> > > exceed four million, find the sum of the even-valued terms.
> > > 
> > > Here is the specification for the second problem:
> > > 
> > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > master/projects/MEDIUM/PEULER/P2/P2.sats
> > > 
> > > Any solutions/implementations 🙂
> > > 
> > > On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:
> > > 
> > > > Here is the link to Project Euler:
> > > > 
> > > > [https://projecteuler.net](https://projecteuler.net)
> > > > 
> > > > In the past, I found it quite interesting to solve in ATS some of the  
> > > > problems published  
> > > > at Project Euler. This can also be particularly effective for teaching  
> > > > oneself various concepts  
> > > > of program verification.
> > > > 
> > > > I have just set up the following ATS-project:
> > > > 
> > > > [https://github.com/githwxi/ATS-Postiats-contrib/tree/](https://github.com/githwxi/ATS-Postiats-contrib/tree/)  
> > > > master/projects/MEDIUM/PEULER
> > > > 
> > > > I hope that the ATS community will have a considerably significant  
> > > > amount of interest in this  
> > > > so that this effort can continue in a meaningful way.
> > > > 
> > > > Let me take the first problem ([#1 Multiples of $3$ or $5$ - Project Euler](https://projecteuler.net/problem=1)) as  
> > > > an example:
> > > > 
> > > > If we list all the natural numbers below 10 that are multiples of 3 or  
> > > > 5, we get 3, 5, 6 and 9. The sum of these multiples is 23.
> > > > 
> > > > Find the sum of all the multiples of 3 or 5 below 1000.
> > > > 
> > > > I give a specification of this problem in the following file:  
> > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > master/projects/MEDIUM/PEULER/P1/P1.sats
> > > > 
> > > > This specification has been implemented in the following file:
> > > > 
> > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats
> > > > 
> > > > In general, a problem can have multiple specifications and each  
> > > > specification can have multiple solutions  
> > > > (that is, implementations).
> > > > 
> > > > I hope that people interested in this will contribute both  
> > > > specifications and solutions. As a community, we  
> > > > can review them together and likely improve them as well.
> > > > 
> > > > At this point, I would like to mostly work as a reviewer/editor. If you  
> > > > contribute, please send your code to  
> > > > this list or to me directly.
> > > > 
> > > > The following link leads to a solution to the first problem that can be  
> > > > type-checked using Patsopt-as-a-service  
> > > > (Patsoptaas):
> > > > 
> > > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_)  
> > > > serve.php?mycode\_url=[https://raw.githubusercontent.com/](https://raw.githubusercontent.com/)  
> > > > githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/  
> > > > P1//P1-hwxi.dats
> > > > 
> > > > The following link leads to a variant of the above solution that can be  
> > > > tested (that is, run) using Patsopt-as-a-service:
> > > > 
> > > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_)  
> > > > serve.php?mycode\_url=[https://raw.githubusercontent.com/](https://raw.githubusercontent.com/)  
> > > > githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/  
> > > > P1/JS/P1-hwxi.dats
> > > > 
> > > > Cheers!
> > > > 
> > > > –  
> > > > You received this message because you are subscribed to the Google Groups  
> > > > “ats-lang-users” group.  
> > > > To unsubscribe from this group and stop receiving emails from it, send an  
> > > > email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > To view this discussion on the web visit  
> > > > [https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com)  
> > > > [https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > .

Brandon Barker  
[brandon...@gmail.com](mailto:brandon...@gmail.com)

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 16, 2015, 6:40am UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253/5 "2015-01-16T06:40:36Z")

</div>

> > Then again, proving something by accident unintentionally may be rare as  
> > well.

I don’t remember encountering any for all these (10?) years.On Fri, Jan 16, 2015 at 1:33 AM, Brandon Barker [brandon...@gmail.com](mailto:brandon...@gmail.com) wrote:

> This does seem like a good way to learn ATS/LF, but at the risk of  
> sounding obtuse, after staring at the specification of P1 a while, I have  
> to wonder if it would be necessary to write an implementation to prove my  
> specification ;). I think Knuth has an applicable quote here, so it can’t  
> hurt at least. The typechecker can only prove coherency, not that I haven’t  
> proved something else, after all.
> 
> Then again, proving something by accident unintentionally may be rare as  
> well.
> 
> All that said, I guess as is pointed out in the ATS book, you probably get  
> used to these recursive proofs after a while.
> 
> On Wed, Jan 14, 2015 at 11:34 PM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> 
> > FYI.
> > 
> > I wrote a README available here:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER)
> > 
> > On Wednesday, January 14, 2015 at 6:56:10 PM UTC-5, gmhwxi wrote:
> > 
> > > FYI.
> > > 
> > > Problem 16
> > > 
> > > 2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.
> > > 
> > > What is the sum of the digits of the number 2^1000?
> > > 
> > > Here is the specification for this problem:
> > > 
> > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > master/projects/MEDIUM/PEULER/P16/P16.sats
> > > 
> > > Note that the specification in P16.sats is not yet a “full”  
> > > specification. If there is some interest, we could  
> > > do one later.
> > > 
> > > On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:
> > > 
> > > > FYI.
> > > > 
> > > > Even Fibonacci numbers
> > > > 
> > > > Problem 2
> > > > 
> > > > Each new term in the Fibonacci sequence is generated by adding the  
> > > > previous two terms. By starting with 1 and 2, the first 10 terms will  
> > > > be:
> > > > 
> > > > 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …
> > > > 
> > > > By considering the terms in the Fibonacci sequence whose values do not  
> > > > exceed four million, find the sum of the even-valued terms.
> > > > 
> > > > Here is the specification for the second problem:
> > > > 
> > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > master/projects/MEDIUM/PEULER/P2/P2.sats
> > > > 
> > > > Any solutions/implementations 🙂
> > > > 
> > > > On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:
> > > > 
> > > > > Here is the link to Project Euler:
> > > > > 
> > > > > [https://projecteuler.net](https://projecteuler.net)
> > > > > 
> > > > > In the past, I found it quite interesting to solve in ATS some of the  
> > > > > problems published  
> > > > > at Project Euler. This can also be particularly effective for teaching  
> > > > > oneself various concepts  
> > > > > of program verification.
> > > > > 
> > > > > I have just set up the following ATS-project:
> > > > > 
> > > > > [https://github.com/githwxi/ATS-Postiats-contrib/tree/](https://github.com/githwxi/ATS-Postiats-contrib/tree/)  
> > > > > master/projects/MEDIUM/PEULER
> > > > > 
> > > > > I hope that the ATS community will have a considerably significant  
> > > > > amount of interest in this  
> > > > > so that this effort can continue in a meaningful way.
> > > > > 
> > > > > Let me take the first problem ([#1 Multiples of $3$ or $5$ - Project Euler](https://projecteuler.net/problem=1)) as  
> > > > > an example:
> > > > > 
> > > > > If we list all the natural numbers below 10 that are multiples of 3 or  
> > > > > 5, we get 3, 5, 6 and 9. The sum of these multiples is 23.
> > > > > 
> > > > > Find the sum of all the multiples of 3 or 5 below 1000.
> > > > > 
> > > > > I give a specification of this problem in the following file:  
> > > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > > master/projects/MEDIUM/PEULER/P1/P1.sats
> > > > > 
> > > > > This specification has been implemented in the following file:
> > > > > 
> > > > > [https://github.com/githwxi/ATS-Postiats-contrib/blob/](https://github.com/githwxi/ATS-Postiats-contrib/blob/)  
> > > > > master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats
> > > > > 
> > > > > In general, a problem can have multiple specifications and each  
> > > > > specification can have multiple solutions  
> > > > > (that is, implementations).
> > > > > 
> > > > > I hope that people interested in this will contribute both  
> > > > > specifications and solutions. As a community, we  
> > > > > can review them together and likely improve them as well.
> > > > > 
> > > > > At this point, I would like to mostly work as a reviewer/editor. If  
> > > > > you contribute, please send your code to  
> > > > > this list or to me directly.
> > > > > 
> > > > > The following link leads to a solution to the first problem that can  
> > > > > be type-checked using Patsopt-as-a-service  
> > > > > (Patsoptaas):
> > > > > 
> > > > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_)  
> > > > > serve.php?mycode\_url=[https://raw.githubusercontent.com/](https://raw.githubusercontent.com/)  
> > > > > githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/  
> > > > > P1//P1-hwxi.dats
> > > > > 
> > > > > The following link leads to a variant of the above solution that can  
> > > > > be tested (that is, run) using Patsopt-as-a-service:
> > > > > 
> > > > > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_)  
> > > > > serve.php?mycode\_url=[https://raw.githubusercontent.com/](https://raw.githubusercontent.com/)  
> > > > > githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/  
> > > > > P1/JS/P1-hwxi.dats
> > > > > 
> > > > > Cheers!
> > > > > 
> > > > > –  
> > > > > You received this message because you are subscribed to the Google Groups  
> > > > > “ats-lang-users” group.  
> > > > > To unsubscribe from this group and stop receiving emails from it, send an  
> > > > > email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> > > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> > > > > To view this discussion on the web visit  
> > > > > [https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com)  
> > > > > [https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/48de36c9-dc01-494a-a015-bd34ae0ea7f1%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > .
> 
> –  
> Brandon Barker  
> [brandon...@gmail.com](mailto:brandon...@gmail.com)
> 
> –  
> You received this message because you are subscribed to the Google Groups  
> “ats-lang-users” group.  
> To unsubscribe from this group and stop receiving emails from it, send an  
> email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrXs\_Qux4K6SL22en-uOnXeJM1MzZ89eKjZKecqwM5j6w%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrXs_Qux4K6SL22en-uOnXeJM1MzZ89eKjZKecqwM5j6w%40mail.gmail.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrXs\_Qux4K6SL22en-uOnXeJM1MzZ89eKjZKecqwM5j6w%40mail.gmail.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/CAORbNRrXs_Qux4K6SL22en-uOnXeJM1MzZ89eKjZKecqwM5j6w%40mail.gmail.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 14, 2015, 5:33am UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253/6 "2015-01-14T05:33:57Z")

</div>

FYI.

Even Fibonacci numbers

Problem 2

Each new term in the Fibonacci sequence is generated by adding the previous  
two terms. By starting with 1 and 2, the first 10 terms will be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …

By considering the terms in the Fibonacci sequence whose values do not  
exceed four million, find the sum of the even-valued terms.

Here is the specification for the second problem:

> <https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P2/P2.sats>

Any solutions/implementations :)On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:

> Here is the link to Project Euler:
> 
> [https://projecteuler.net](https://projecteuler.net)
> 
> In the past, I found it quite interesting to solve in ATS some of the  
> problems published  
> at Project Euler. This can also be particularly effective for teaching  
> oneself various concepts  
> of program verification.
> 
> I have just set up the following ATS-project:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER)
> 
> I hope that the ATS community will have a considerably significant amount  
> of interest in this  
> so that this effort can continue in a meaningful way.
> 
> Let me take the first problem ([#1 Multiples of $3$ or $5$ - Project Euler](https://projecteuler.net/problem=1)) as an  
> example:
> 
> If we list all the natural numbers below 10 that are multiples of 3 or 5,  
> we get 3, 5, 6 and 9. The sum of these multiples is 23.
> 
> Find the sum of all the multiples of 3 or 5 below 1000.
> 
> I give a specification of this problem in the following file:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats)
> 
> This specification has been implemented in the following file:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats)
> 
> In general, a problem can have multiple specifications and each  
> specification can have multiple solutions  
> (that is, implementations).
> 
> I hope that people interested in this will contribute both specifications  
> and solutions. As a community, we  
> can review them together and likely improve them as well.
> 
> At this point, I would like to mostly work as a reviewer/editor. If you  
> contribute, please send your code to  
> this list or to me directly.
> 
> The following link leads to a solution to the first problem that can be  
> type-checked using Patsopt-as-a-service  
> (Patsoptaas):
> 
> [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats)
> 
> The following link leads to a variant of the above solution that can be  
> tested (that is, run) using Patsopt-as-a-service:
> 
> [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats)
> 
> Cheers!

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 14, 2015, 11:56pm UTC](https://discourse.ats-lang.org/t/trying-project-euler-in-ats/253/7 "2015-01-14T23:56:10Z")

</div>

FYI.

Problem 16

2^15 = 32768 and the sum of its digits is 3 + 2 + 7 + 6 + 8 = 26.

What is the sum of the digits of the number 2^1000?

Here is the specification for this problem:

> <https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P16/P16.sats>

Note that the specification in P16.sats is not yet a “full” specification.  
If there is some interest, we could  
do one later.On Wednesday, January 14, 2015 at 12:33:57 AM UTC-5, gmhwxi wrote:

> FYI.
> 
> Even Fibonacci numbers
> 
> Problem 2
> 
> Each new term in the Fibonacci sequence is generated by adding the  
> previous two terms. By starting with 1 and 2, the first 10 terms will be:
> 
> 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, …
> 
> By considering the terms in the Fibonacci sequence whose values do not  
> exceed four million, find the sum of the even-valued terms.
> 
> Here is the specification for the second problem:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P2/P2.sats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P2/P2.sats)
> 
> Any solutions/implementations 🙂
> 
> On Tuesday, January 13, 2015 at 7:21:22 PM UTC-5, gmhwxi wrote:
> 
> > Here is the link to Project Euler:
> > 
> > [https://projecteuler.net](https://projecteuler.net)
> > 
> > In the past, I found it quite interesting to solve in ATS some of the  
> > problems published  
> > at Project Euler. This can also be particularly effective for teaching  
> > oneself various concepts  
> > of program verification.
> > 
> > I have just set up the following ATS-project:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/PEULER)
> > 
> > I hope that the ATS community will have a considerably significant amount  
> > of interest in this  
> > so that this effort can continue in a meaningful way.
> > 
> > Let me take the first problem ([#1 Multiples of $3$ or $5$ - Project Euler](https://projecteuler.net/problem=1)) as an  
> > example:
> > 
> > If we list all the natural numbers below 10 that are multiples of 3 or 5,  
> > we get 3, 5, 6 and 9. The sum of these multiples is 23.
> > 
> > Find the sum of all the multiples of 3 or 5 below 1000.
> > 
> > I give a specification of this problem in the following file:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1.sats)
> > 
> > This specification has been implemented in the following file:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats](https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/PEULER/P1/P1-hwxi.dats)
> > 
> > In general, a problem can have multiple specifications and each  
> > specification can have multiple solutions  
> > (that is, implementations).
> > 
> > I hope that people interested in this will contribute both specifications  
> > and solutions. As a community, we  
> > can review them together and likely improve them as well.
> > 
> > At this point, I would like to mostly work as a reviewer/editor. If you  
> > contribute, please send your code to  
> > this list or to me directly.
> > 
> > The following link leads to a solution to the first problem that can be  
> > type-checked using Patsopt-as-a-service  
> > (Patsoptaas):
> > 
> > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1//P1-hwxi.dats)
> > 
> > The following link leads to a variant of the above solution that can be  
> > tested (that is, run) using Patsopt-as-a-service:
> > 
> > [http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas\_serve.php?mycode\_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats-contrib/master/projects/MEDIUM/PEULER/P1/JS/P1-hwxi.dats)
> > 
> > Cheers!