Natural Number Game in Dafny (and possibly other languages)

Stream: general

[Huỳnh Trần Khanh]

Is anyone in here interested in NNG in other verification languages?

[Huỳnh Trần Khanh]

I know Dafny and also a little bit about compiling software for the web so I can help port this stuff to Dafny (if you want).

[Mario Carneiro]

I'm not sure that the tasks in NNG necessarily fit as a software verification exercise

[Mario Carneiro]

I would expect something more like https://github.com/hwayne/lets-prove-leftpad

[Mario Carneiro]

(speaking of which: has anyone proved left pad correct in lean yet?)

[Alex J. Best]

leanprover is on the list in that repo

[Mario Carneiro]

oops, silly question