> without code
Excel is a programming language. Change my mind
6
6
28
Conversation
Potentially more controversial take: PowerPoint animations are a (very inconvenient) programming language
1
9
ms powerpoint was proven turing complete this is more like a fact than a take imo
2
2
A programming language doesn’t have to be Turing-complete though! In fact many highly formal functional and logic programming languages are deliberately *not* Turing-complete to improve their theoretical properties.
1
1
1
oh fascinating, can you give me an example to investigate?
1
I believe Isabelle/HOL is not Turing-complete but don’t quote me on that. For a while many people believed Idris wasn’t, but a proof came out late last year
1
2
ah apparently proofs have existed for a while, but I don’t know enough about Idris to say more
1
1
Replying to
Tbf I think that is more of a bug in Idris though. It’s a pretty hard thing to get right in a complicated surface language - Agda is often found to have these kinds of bugs in its totality checker.
Replying to
Complicated in terms of supporting mutual definitions/inductive recursive types, cumulative universes, etc, and trying not to get in your way as much as possible.
1