On Wed, Jul 20, 2016 at 12:08:29AM +0900, Akira Yokosawa wrote: > On 2016/07/19 23:42 +0900, Akira Yokosawa wrote: > > Hi Paul, > > These are typos I noticed while reading recently updated part in "formal/formal.tex". > > > Furthermore, although the L4 microkernel is a large software > > artifact from the viewpoint of formal verification, it is tiny > > - compared to the a great number of projects, including LLVM, > > + compared to a great number of projects, including LLVM, > > Here, "the" and "a" are redundant. I removed "the", because I have no idea > how many projects are there in this context. > > > gcc, the Linux kernel, Hadoop, MongoDB, and a great many others. > > > > Although formal verification is finally starting to show some > > @@ -171,4 +171,4 @@ All else being equal, a simpler implementation is much better than > > a mechanical proof for a complex implementation! > > > > And the open challenge to those working on formal verification techniques > > -and systems is prove this summary wrong! > > +and systems is to prove this summary wrong! > > > > This seems a trivial one. Agreed on both, pulled and pushed. And thank you for your careful review and the fixes! Thanx, Paul -- To unsubscribe from this list: send the line "unsubscribe perfbook" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
