Ask HN: What was the best CS paper you read in 2017?
I read a lot of good ones but I&#x27;ll answer what was <i>most important</i> rather than best. We&#x27;re seeing a revival of formal methods ranging from lightweight (TLA+) to heavy. Two problems are in my sight: lack of framework plus consistent, empirical data for evaluating how suitable a given method is for a specific project or company; many who would use lightweight or practical methods will quit because someone convinced them to start with heavy ones. The paper below is a start on the former:<p><a href="https:&#x2F;&#x2F;www.scch.at&#x2F;de&#x2F;rse-news&#x2F;passende-formale-methon?file=files&#x2F;Dokumente&#x2F;SCCH_Web&#x2F;Downloads&#x2F;Downloads_2015&#x2F;DownloadBilder&#x2F;Neu_SCCH-TR-1603_FormalMethodsComparison.pdf" rel="nofollow">https:&#x2F;&#x2F;www.scch.at&#x2F;de&#x2F;rse-news&#x2F;passende-formale-methon?file...</a><p>I think that was a great start on an evalution criteria because its comparisons match what I read in the various experience reports. ASM&#x27;s and TLA+ coming in the lead on usability but B method on code generation. It will also help to note what projects have been completed or reusable libraries available in each. A person building verified compilers for functional languages might want to learn Isabelle&#x2F;HOL due to CakeML, doing a new TLS extension learn F* due to miTLS, type-safe assembly learn Coq due to CoqASM, and so on.<p>For the other issue, I made a proposal on HN first and then on Lobste.rs about avoiding people quitting early from finding formal methods too overwhelming or useless. I proposed having a default intro or lure that matched the goals of different people to tools with a warning of some&#x27;s difficulty. It got some interesting responses (below) I&#x27;ll turn into a mini-essay with links eventually.<p><a href="https:&#x2F;&#x2F;lobste.rs&#x2F;s&#x2F;n7v658&#x2F;your_thoughts_on_this_advice_those" rel="nofollow">https:&#x2F;&#x2F;lobste.rs&#x2F;s&#x2F;n7v658&#x2F;your_thoughts_on_this_advice_thos...</a>