jamster02

> the Unicode string "√5" is representable as 4 UTF-8 bytes

As the other person pointed out, this is representing an irrational number unambiguously in a finite number of bits (8 bits in a byte). I fail to see how your original statement was careful :)

> representable in a finite number of digits or bits

I also recently ran into a problem when unit testing and monkey patching where I had to import after monkey patching, so in the function itself.

The fact that it is no longer peasant food doesn't consciously play any part in that.

I appreciate even more ideas to work with. A more "working" proof language sounds interesting. While I agree that Rocq is decidably not for a "working programmer," I've had a lot of fun working through the book "Software Foundations". Last night, I was able to formally prove the pumping lemma for regular languages, and that was very satisfying and enjoyable. Another reason I'm learning Rocq is due to my (largely uninformed) interest in homotopy type theory.

I appreciate the resources and recommendations. I've been interesting in Rocq (formerly Coq) recently, and I've seen dependent types mentioned, so I've been curious to learn more.

Regex isn't (necessarily) turing complete :)

> Because our program just consists of a sequence of regular expressions, you can't loop at all! That, technically, means we can't actually perform Turing Complete But we can do any bounded computation by just unrolling any loops we may have.

Although some (most?) implementations may be. Though by the above quote, the author didn't make use of that.