Ancestors

Written by Edwin Brady on 2024-11-06 at 00:19

I often read on the Internet - and I realise that I should know by now that it's not a good place to read things - that Idris isn't Turing Complete and can't be because it's dependently typed. I think I can guess where this idea comes from, but, in case of any doubt, it's Turing Complete. Of course it's Turing Complete. For goodness sake...

=> More informations about this toot | More toots from edwinb@types.pl

Written by Edwin Brady on 2024-11-06 at 00:21

I once implemented Whitespace in Idris because I was the right sort of bored. People are happy to believe Whitespace is Turing Complete but Idris? No, couldn't possibly be, I mean it's dependently typed isn't it? (Of course it is. Stop it.)

=> More informations about this toot | More toots from edwinb@types.pl

Written by Edwin Brady on 2024-11-06 at 00:24

Turing Completeness is overrated anyway. Pacman Completeness is where it's at.

=> More informations about this toot | More toots from edwinb@types.pl

Toot

Written by Tristram Brelstaff on 2024-11-28 at 18:18

@edwinb Admit it: you only say that because Pacman completeness is much more fun to test than Turing completeness!

=> More informations about this toot | More toots from tristrambrelstaff@mathstodon.xyz

Descendants