Re:CVE-2021-32471 – Input validation in Marvin Minsky 1967 T...
by ludamad on Monday May 10, 2021 @09:30AM
(#27105770)
A non-TC language can be achieved just by forcing proofs. Oh, you want that program to run? Just prove that it is bounded memory and can't halt, etc
[ Parent
| on HN ]
Re:CVE-2021-32471 – Input validation in Marvin Minsky 1967 T...
by qsort on Monday May 10, 2021 @09:38AM
(#27105847)
Yeah, but that's the 'cumbersome' part. Could we imagine a non-TC language with simple syntax that's suitable for at least some of the task you'd use a TC language for?
Re:CVE-2021-32471 – Input validation in Marvin Minsky 1967 T...
by magmastonealex on Monday May 10, 2021 @12:03PM
(#27107533)
C compiled down to eBPF (as implemented with the Linux kernel) is not turing-complete. eBPF has a wide variety of uses from network filtering to hooking into certain syscalls.
The bytecode is theoretically turing-complete, but the verifier present in the kernel ensures that the code contains no loops and accesses no out-of-bounds memory.
With `clang`, you can compile C down to eBPF bytecode. It's a subset of C, with a lot of restrictions, but it is familiar and capable of some remarkable things past just simple packet parsing & filtering.
Re:CVE-2021-32471 – Input validation in Marvin Minsky 1967 T...
by qsort on Monday May 10, 2021 @12:15PM
(#27107659)
I had no idea, this is fascinating. Thanks for sharing.
Re:CVE-2021-32471 – Input validation in Marvin Minsky 1967 T...
by UncleMeat on Monday May 10, 2021 @11:38AM
(#27107218)
A useful subset of SQL is not turing-complete and is suitable for meaningful computational tasks. Datalog is also not turing-complete and is similarly useful.
Re:CVE-2021-32471 – Input validation in Marvin Minsky 1967 T...
by qsort on Monday May 10, 2021 @11:46AM
(#27107326)
Sure, more examples are CSP solvers and AMPL. They are all somewhat specific though. I was wondering if it would be possible to make one that's "general purpose" in the same sense you call programming languages "general purpose", i.e. one you'd write application software in.