Humans have been creating more and more proofs for the benefit of computers. They're just not recognized as such because these efforts are independent of mainstream mathematics.
It's called computer programming. The Curry-Howard correspondence demonstrates that
every program in a statically typed language
represents a proof, with the same kind of formality as the mathematical proofs mentioned in the article.
The outages... highlight why the state's various websites should be brought under one authority, said Leroy Williams, the state's secretary of technology.
So then one flaw can take down the government of Colorado's, not just the Secretary of State's website.
I've seen Chaitin present a paper on register allocation. He skilfully held the attention of the entire audience. It wouldn't be surprising if this were a real page turner.
Yes, he's the same register allocation by graph coloring Chaitin. Compilers aren't a particular interest of his -- he just happened upon some compiler people working on the problem and helped come up with an interesting approach.
Slashdot Mirror
Humans have been creating more and more proofs for the benefit of computers. They're just not recognized as such because these efforts are independent of mainstream mathematics.
It's called computer programming. The Curry-Howard correspondence demonstrates that every program in a statically typed language represents a proof, with the same kind of formality as the mathematical proofs mentioned in the article.
I've seen Chaitin present a paper on register allocation. He skilfully held the attention of the entire audience. It wouldn't be surprising if this were a real page turner.
Yes, he's the same register allocation by graph coloring Chaitin. Compilers aren't a particular interest of his -- he just happened upon some compiler people working on the problem and helped come up with an interesting approach.
The Register says examples of the technologies Microsoft is licensing are SMB and CIFS.