3 ms·
It was a joke. I didn’t know that about Hamilton, though. In case her work interests you, I did get their book on Higher Order Software where she applied every
by nickpsecurity 3y ago
It was a joke. I didn’t know that about Hamilton, though.
In case her work interests you, I did get their book on Higher Order Software where she applied everything they learned. The method was like executable specifications with code generators. The specs were reminiscient of Prolog and CSP mixed together. Later, it became USL in the 001 Toolkit. It and her other papers are on htius.com.
I didn’t think HOS/USL was practical. Her team’s early work was really impressive, though. I also still respect everyone that tried to achieve the hard goal of formally-specified, bug-proof software. Each attempt teaches us lessons.
- EdwardCoffin 3y agoDo you have a link for Higher Order Software perhaps? I couldn't find it on htius.com
- nickpsecurity 3y agoI had to dig it up out of my order history for you. Here is the HOS book. I've included a preview link that shows the Table of Contents. System Design from Provably Correct Constructs: The Beginnings of True Software Engineering by James Martin https://www.amazon.com/gp/product/013881483X/ref=ppx_yo_dt_b_search_asin_title?ie=UTF8&psc=1 https://www.amazon.com/gp/product/013881483X/ref=ppx_yo_dt_b... https://archive.org/details/systemdesignfrom00mart/page/n3/mode/2up https://archive.org/details/systemdesignfrom00mart/page/n3/m... Now, if you want a practical method, the best were Design by Contract, Cleanroom Software Engineering, and Praxis' Correct by Construction. Cleanroom and CbyC hit very, low, defect rates. DbyC was highly pragmatic in balancing developer productivity, ease of adoption, and correctness. I think they'd all be even better combined with functional programming, static, test generators, etc. that we now have. In any case, here's links to descriptions of and books on some of those methods. Design by Contract article https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... Overview of Cleanroom Method https://ifs.host.cs.st-andrews.ac.uk/Books/SE9/Web/Cleanroom/ https://ifs.host.cs.st-andrews.ac.uk/Books/SE9/Web/Cleanroom... Book teaching Cleanroom https://www.amazon.com/gp/product/0201385953/ref=ppx_yo_dt_b_search_asin_title?ie=UTF8&psc=1 https://www.amazon.com/gp/product/0201385953/ref=ppx_yo_dt_b... Overview of Praxis Correct by Construction https://elsmar.com/pdf_files/A%20Manifesto%20for%20High-Integrity%20Software.pdf https://elsmar.com/pdf_files/A%20Manifesto%20for%20High-Inte... Book teaching SPARK Ada with some CbyC https://www.amazon.com/gp/product/1107656842/ref=ppx_yo_dt_b_search_asin_title?ie=UTF8&psc=1 https://www.amazon.com/gp/product/1107656842/ref=ppx_yo_dt_b... Abstract, State Machines and the B Method had many successful, industrial uses. There's many papers on them.
- EdwardCoffin 3y agoWow, thanks for all the links. I hadn't realized you really meant book - I thought by their book on Higher Order Software you meant Hamilton's and Zeldin's paper Higher Order Software—A Methodology for Defining Software [1], which I managed to get through the local university library. [1] https://ieeexplore.ieee.org/document/1702333 https://ieeexplore.ieee.org/document/1702333
- nickpsecurity 3y agoI didn’t know about that one. Thanks for it.