How did software get so reliable without proof? (1996) [pdf]
6826.csail.mit.edu
6826.csail.mit.edu
How Did Software Get So Reliable Without Proof? (1996) [pdf] - https://news.ycombinator.com/item?id=24503153 - Sept 2020 (123 comments)
How did software get so reliable without proof? - https://news.ycombinator.com/item?id=22478585 - March 2020 (130 comments)
How did software get so reliable without proof? (1996) [pdf] - https://news.ycombinator.com/item?id=18050706 - Sept 2018 (33 comments)
How Did Software Get So Reliable Without Proof? (1996) [pdf] - https://news.ycombinator.com/item?id=11293881 - March 2016 (82 comments)
> Abstract: By surveying current software engineering practice, this paper reveals that the techniques employed to achieve reliability are little different from those which have proved effective in all other branches of modern engineering: rigorous management of procedures for design inspection and review; quality assurance based on a wide range of targeted tests; continuous evolution by removal of errors from products already in widespread use; and defensive programming, among other forms of deliberate over-engineering. Formal methods and proof play a small direct role in large scale programming; but they do provide a conceptual framework and basic under- standing to promote the best of current practice, and point directions for future improvement.
From "Extreme Programming" > History: https://en.wikipedia.org/wiki/Extreme_programming :
> He began to refine the development methodology used in the project [in 1996] and wrote a book on the methodology (Extreme Programming Explained, published in October 1999)
> Many extreme-programming practices have been around for some time; the methodology takes "best practices" to extreme levels. For example, the "practice of test-first development, planning and writing tests before each micro-increment" was used as early as NASA's Project Mercury, in the early 1960s.
Agile > History: https://en.wikipedia.org/wiki/Agile_software_development#His... :
> Iterative and incremental software development methods can be traced back as early as 1957, [10] with evolutionary project management [11][12] and adaptive software development [[ ASD ]] emerging in the early 1970s.
> During the 1990s, a number of lightweight software development methods evolved in reaction to the prevailing heavyweight methods (often referred to collectively as waterfall) that critics described as overly regulated, planned, and micromanaged. [15] These lightweight methods included: rapid application development (RAD), from 1991; [16][17] the unified process (UP) and dynamic systems development method (DSDM), both from 1994; Scrum, from 1995; Crystal Clear and extreme programming (XP), both from 1996; and feature-driven development (FDD), from 1997. Although these all originated before the publication of the Agile Manifesto, they are now collectively referred to as agile software development methods. [3]
> "Manifesto for Agile Software Development" [2001]
awesome-safety-critical: https://awesome-safety-critical.readthedocs.io/en/latest/
/? z3
From https://news.ycombinator.com/item?id=41944043 :
> - Does Z3 distinguish between xy+z and z+yx, in terms of floating point output? math.fma() would be a different function call with the same or similar output.
> (deal-solver is a tool for verifying formal implementations in Python with Z3.)
- re: property testing, fuzzing, formal verification: https://news.ycombinator.com/item?id=40884466 https://westurner.github.io/hnlog/#story-40875559
From "The Future of TLA+ [pdf]" (2024) https://news.ycombinator.com/item?id=41385141 :
> Formal methods including TLA+ also can't/don't prevent or can only workaround side channels in hardware and firmware that is not verified. But that's a different layer.
Things formal methods shouldn't be expected to find: Floating point arithmetic non-associativity, side-channels
> "Use of Formal Methods at Amazon Web Services" (2014) https://lamport.azurewebsites.net/tla/formal-methods-amazon....
>> This raised a challenge; how to convey the purpose and benefits of formal methods to an audience of software engineers? Engineers think in terms of debugging rather than ‘verification’, so we called the presentation “Debugging Designs” [8] . Continuing that metaphor, we have found that software engineers more readily grasp the concept and practical value of TLA+ if we dub it:
Exhaustively testable pseudo-code