Re: [PATCH] formal: Trivial typo fixes

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

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