If you read the article it's specifically for concurrency, so you can put asserts about the multitasking properties of the code and you know it's not going to fuck up. It's limited domain. It doesn't mean that whatever code you put in there will magically do what's in your brain, the logic can still have flaws. But this is to solve common multitasking issues specifically.
In the article they say "provably correct", so what they've actually done is code some sort of logic framework that can take code written in this language and tell you a definitive yes/no as to whether it's broken from a concurrency viewpoint.
The halting problem is kind of irrelevant here. What they're saying is that they have a system in place that's provable for a
subdomain which is concurrency. Proving all things is impossible. Proving
some things is definitely possible. Bringing up the halting problem here is like saying you can't plot a line because of Cantor's proof of uncountable infinities.
delphonso, the published work contradicts both of the things you just said:
Parno and a team of researchers recently published a new coding language and tool for high-performance concurrent programs that ensures that programs are provably-correct—that is, that the code is mathematically proven to compute correctly. The language and tool, named Armada, was presented at this year's Conference on Programming Language Design and Implementation, and the paper received a Distinguished Paper award.
I'm kind of guessing that something existing is the proof of concept against the idea that it can't exist.
Pretty much sums up the whole thing.
Author
Topic: Things that made you go "WTF?" today o_O (Read 14888641 times)