[klibertp]

That's the point, I think: for a large number of real-world algorithms, you don't actually need a Turing Machine. There was a very well-written explanation of this on the front page[1] some time ago, concluded with:

> Any algorithm that can be implemented by a Turing Machine such that its runtime is bounded by some primitive recursive function of input can also be implemented by a primitive recursive function!

Also, "The Little Typer" book explores a language based on "primitive recursive functions" and shows what can be done in it and how.

[1] https://matklad.github.io/2024/08/01/primitive-recursive-fun...

[jamster02]

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.

[klibertp]

On that note, I discovered Dafny[1] recently, as a more accessible way to program with proofs. There's a companion book[2] that seems very accessible and down-to-earth (and, unfortunately, quite expensive). I didn't have the time to play with it yet, but it looks like it does what Ada/SPARK does (and more), but with less verbose syntax and more options for compilation targets. It seems to be actively developed, too. Personally, I had a very hard time getting into Coq, which is a proof assistant more than a programming environment - Dafny seems much more welcoming for a "working programmer" :)

[1] https://dafny.org/

[2] https://mitpress.mit.edu/9780262546232/program-proofs

[jamster02]

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.