Re:CompCert - Compilers you can formally trust
by protomyth on Saturday June 04, 2011 @02:17PM
(#2620061)
I seem to remember a CPU that was stack-based that was built for correctness. I think it was called the Viper, but I cannot seem to find it. It would be logical to me to run your formally trusted compiler on a chip designed the same way.
[ Parent
| on HN ]
Re:CompCert - Compilers you can formally trust
by daveasdf on Saturday June 04, 2011 @08:47PM
(#2620905)
You might be thinking of Verisoft and their "VAMP" hardware stack: http://www.verisoft.de/SubProject2.html
The original goal of the project was to have a verified computer stack, with proofs going from the software, compiler and processor all the way down to the gate level.
I am not sure how far they got, but I don't think the project is still active, which is a bit sad.