doc-src/IsarImplementation/implementation.tex
changeset 18554 bff7a1466fe4
parent 18537 2681f9e34390
child 19189 dbc19b772f5b
equal deleted inserted replaced
18553:14f24be9e499 18554:bff7a1466fe4
    47 % Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
    47 % Not everyone likes this idea. Specification experts rightly abhor trial-and-error programming.
    48 % They suggest that no one should write a program without First writing a complete
    48 % They suggest that no one should write a program without First writing a complete
    49 % formal specification. But university departments are not software houses. Programs like
    49 % formal specification. But university departments are not software houses. Programs like
    50 % Isabelle are not products: when they have served their purpose, they are discarded.
    50 % Isabelle are not products: when they have served their purpose, they are discarded.
    51 %
    51 %
    52 % L.C. Paulson, Isabelle: The Next 700 Theorem Provers
    52 % L.C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
       
    53 
       
    54 % As I did 20 years ago, I still fervently believe that the only way to
       
    55 % make software secure, reliable, and fast is to make it small. Fight
       
    56 % Features.
       
    57 %
       
    58 % Andrew S. Tanenbaum
    53 
    59 
    54 \appendix
    60 \appendix
    55 \input{Thy/document/ML.tex}
    61 \input{Thy/document/ML.tex}
    56 
    62 
    57 \begingroup
    63 \begingroup