As many things Apple does, I think this will not work well world wide. As it is the case of DDG. In my country, Google Maps and Google Search blow everything away.
There are many finite constraints. First, there is no infinite time [1]. The most famous uncomputable problem is the halting problem (given an algorithm A and an input x, can we compute it? that is, will A stop on x?). Although we have an infinite tape, since the time of a computation is finite, the space it uses is also. Second, we describe a Turing machine using finite sets.
[1] Actually, as described by Turing, a Turing machine neves stops, but this is only because he is interested in computing real numbers (for example pi). But even using an original Turing machine, we do not "compute" pi. We only "compute" pi with some precision.
> Nearly a century ago, Alonzo Church invented the simple, elegant, and yet elusive lambda calculus. Along with Alan Turing, he then proved the Church-Turing thesis: that anything computable with a Turing machine can also be computed in the lambda calculus.
The Church-Turing thesis is not something one can prove. It's more like an intuition and/or definition we have. It states that anything that is computable can be computed with a Turing machine. See [1].
"Anything computable with a Turing machine can also be computed in the lambda calculus" this is true but it not the Church-Turing thesis and its called a Turing-equivalence. This was also not proved by Church, but by Turing in an appendix to his paper [2].
About a computation model being Turing-equivalent: the fact that most reasonable computation models we came up with were proven to be Turing-equivalent is one of the reasons we believe in the Church-Turing thesis.
I need to collaborate with other people and because of COVID we are doing everything remote. Also modifications would be hard and time consuming with pencil and paper.
Congratulations, looks like a really nice language.
One nitpick: I think "val" looks too much like "var" and this will make it harder do differentiate them by code skimming. I suggest changing "val" to something like "const", or "fix", or "imm"...
I don't know why but someone edited my comment. The original had 2 footnotes which were combined into one. Now it is ambiguous. Thank you for your disservice.
I think the name is really bad in Brazilian Portuguese. Here "pika"* is a slang for dick. At the same time, it is still the sound Pikachu makes ("pika pika"). So maybe there is no problem.
* I don't know about European Portuguese.
The correct spelling for the slang would be "pica", but both have the same pronunciation.
> This was probaly funny for the writer, but is almost never a good idea, since the image makes no more sense as soon as you switch languages
He is writing in English why should he be preoccupied if it does not make sense in other languages. There are many English expressions that have no exact translations. Should writers avoid using these expressions too?
Also, as a curiosity, terminal has the same ambiguity in Brazilian Portuguese