2010-03-02
by earl, 5378 days ago
"Compcert is a [verified] compiler that generates PPC and ARM assembly code from a large subset of the C programming language. The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its correctness was entirely proved."Extremely impressive work by [create Xavier Leroy] et al.
Jon Stokes: "Perhaps [the] most likely reason behind Apple's silence, is that the A4 just isn't anything to write home about [..]. If Apple were to tell you what's in the A4, most of the focus would be on what the chip is not, rather than on what the iPad is."
I've got to confess to having indulged in speculations about the A4 in the past. May the above help to finally dispel quad-core-featuring myths. Even if reality will catch up with those in a month or so anyway.
search
45 active users
- unknown (45)
backlinks (more)
none, yet
recent stores (more)
recent comments
echo earlZstrainYat|tr ZY @.
