An important issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method in software development. A fundamental assumption in this talk is that many of the analyses made possible by formal methods research do not require advanced mathematical training and theorem proving skills. I also argue that more ``practical" formal methods are needed, i.e., methods that have a solid mathematical foundation but do not require advanced mathematical training. Two critical attributes of a "practical" formal method are 1) a user-friendly notation for specifying the required system behavior and 2) a set of tools that detect many classes of errors automatically and provide feedback useful in error correction. Examples of additional research (e.g., automatic abstraction methods and automatic generation of invariants) that can help make current formal methods more useful in practical software development are proposed. Also suggested are tool features that would encourage more widespread use of formal methods by practitioners. To illustrate these ideas, I will present examples based on the SCR (Software Cost Reduction) requirements method and describe lessons learned applying the SCR method to several real-world systems.