Top all-time · #1937
Ron Pressler
Personal blog · pron.github.io/posts · on HN as pronprogrammingmath
Ron Pressler's personal blog at pron.github.io covers programming and math. Since 2017, 37 different Hacker News readers have linked it 140 times, most often “Why writing correct software is hard”. The last post was in 2018, but the archive is still widely read.
Too few sampled comments (26) to say how often HN recommends it.?
Why HN links it
HN readers link Ron Pressler's blog for its TLA+ introductions and its essays on correctness and complexity, which commenters cite as the standard argument on why verification has limits.
Summarised by Claude from a sample of 26 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
Ron Pressler's blog
Most-linked posts?
- Why writing correct software is hard8 people · 28 mentions · first linked 2017-05-28
- Finite of Sense and Infinite of Thought7 people · 7 mentions · first linked 2018-01-05
- Principles of TLA+5 people · 7 mentions · first linked 2017-05-28
- History of Computation, Logic and Algebra4 people · 12 mentions · first linked 2018-01-19
- /tlaplus4 people · 11 mentions · first linked 2018-09-24
- People Don't Write Programs4 people · 10 mentions · first linked 2018-09-27
- What We Talk About When We Talk About Computation4 people · 4 mentions · first linked 2018-11-23
- TLA+ in Practice and Theory, Part 2: The + in TLA+3 people · 5 mentions · first linked 2017-06-03
- /2 people · 11 mentions · first linked 2018-12-27
- /2 people · 9 mentions · first linked 2017-08-07
What Hacker News says?
> There's no obvious barrier to it It's like saying that there's no barrier to turning lead into gold except for the fact that it's easier to get gold by other means; that's a good thing! The cost of deriving formal deductive proofs is high, while unsound methods are much cheaper and highly effective. The reason proofs can be expensive is that proving things has an intrinsic computational complexity cost (it's a sea…
Comment linking /posts/correctness-and-complexity
on “Fast”Submitted TLA+ in Practice and Theory, Part 4: Order in TLA+ as a story · 143 points
HN discussionThe article only discusses reasons why formal verification is needed. It does not provide any information on how would AI solve the fundamental issues making it difficult: https://pron.github.io/posts/correctness-and-complexity
Comment linking /posts/correctness-and-complexity
on “AI will make formal verification go mainstream”Submitted TLA+ in Practice and Theory, Part 3: The Temporal Logic of Actions as a story · 130 points
HN discussion> but surely you can see that experienced software developers have somewhat more basis to make claims about type systems But experienced software developers, more than "random people", should know that if they make a conjecture, it's tested and isn't verified, they should reconsider their conjecture. > You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopa…
Comment linking /
on “Correctness and composability bugs in the Julia ecosystem”Submitted Principles of TLA+ as a story · 121 points
HN discussionBy no means a textbook, just a barely-edited book-length anthology of primary sources I put together, but let me plug my own: Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra https://pron.github.io/computation-logic-algebra
Comment linking /computation-logic-algebra
on “Computer Science textbooks that are freely available online”Submitted TLA+ in Practice and Theory, Part 2: The + in TLA+ as a story · 66 points
HN discussionTLA is one of the systems that are actually very practical. You can go up or down as many abstraction layers as you need . There's a great introduction written by @pron on his blog [1]. However, it's worth pointing out that you don't magically get the final program out of the TLA proof. The proof only works for the abstraction level that you chose to write it at. [1] https://pron.github.io/
Comment linking /
on “Software Engineering ≠ Computer Science (2009)”Submitted Finite of Sense and Infinite of Thought as a story · 37 points
HN discussion> so there is no plausible reason for you to infer that I was talking about Heartbleed. Except that Heartbleed is the only OpenSSL bug I've heard of :) Also, I don't know who Kurt Roeckx is. > there's a lot of evidence from software project metrics that the cost of modifying software can easily exceed the cost of rewriting it But we're not talking about arbitrary modification, but about, at worst, fixing undefined b…
Comment linking /posts/correctness-and-complexity
on “How to not rewrite it in Rust”Submitted A History of Computation, Logic and Algebra, Part I as a story · 15 points
HN discussionI find TLA+ syntax and tooling to be far better than that of almost all programming languages. E.g., here's a TLA+ spec I recently wrote: https://pron.github.io/files/TicTacToe.pdf The syntax is as close to standard informal mathematical notation as formality can afford.
Comment linking /files/TicTacToe.pdf
on “Why Don't People Use Formal Methods?”Submitted History of Computation, Logic and Algebra as a story · 8 points
HN discussionTLA+ uses an almost-standard mathematical notation, so that people with some familiarity with mathematics can read it in ~10 minutes of training. You can see examples of what it looks like in my post here ( https://pron.github.io/posts/tlaplus_part2 ) This website chooses to show the ASCII version that you actually type to get the "real" pretty-printed syntax.
Comment linking /posts/tlaplus_part2
on “Learn TLA+ (2018)”Submitted TLA+ in Practice and Theory as a story · 5 points
HN discussion> If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language. That depends on the runtime type system. If you can switch an int for a string (which is not hard in a dependent type system -- rely on the output of some silly arithmetic function that you only tested and omit a proof and use it in some function that indexes types by integers, and you just might cast…
Comment linking /posts/tlaplus_part3
on “Dynamic type systems are not inherently more open”Submitted Why writing correct software is hard as a story · 4 points
HN discussionNo, it is not possible, not only in practice but - more importantly - in theory as well: https://pron.github.io/posts/correctness-and-complexity
Comment linking /posts/correctness-and-complexity
on “What is going on right now?”Submitted What We Talk About When We Talk About Computation as a story · 4 points
HN discussionI usually love Graydon's posts, but this one -- like many articles about formal methods -- may be misleading for most readers unfamiliar with the field. It's a little like reporting an order of magnitude improvement in transmuting lead into gold without mentioning that there are 29 further orders of magnitude to go before the method is cost-effective in practice. Does no aliasing make formal verification significant…
Comment linking /posts/correctness-and-complexity
on “Some notes on Rust, mutable aliasing and formal verification”Submitted A History of Computation, Logic and Algebra as a story · 4 points
HN discussionAlso relevant: https://pron.github.io/tlaplus
Comment linking /tlaplus
on “Learn TLA+”Submitted Why Writing Correct Software Is Hard (2016) as a story · 2 points
HN discussionIt is combinatorial explosion of possible states (not as in memory state of program, but the differing visions of the next state of architecture). Plus high impact of mistakes, suboptimal solutions and randomness when switching between states. Edit: I like this 10 years old blog post in regards to explaining the problem much better than I could do: https://pron.github.io/posts/correctness-and-complexity
Comment linking /posts/correctness-and-complexity
on “Jepsen: ParticleDB 1.1.4”Submitted People Don't Write Programs as a story · 2 points
HN discussion> There is formal specification in the large if you count formal mathematics. Sure, but TLA+ is not aimed at research. The biggest problem, by far, plaguing not just proof assistants but formal logic in general, pretty much since its inception, is complexity. Which is ironic because the entire purpose of formal logic -- from Leibniz's original dream to Frege's early success -- is to be simple, clear and easy tool fo…
Comment linking /
on “The Paxos Algorithm, or How to Win a Turing Award”Submitted What We Talk About When We Talk About Computation as a story · 2 points
HN discussionThis is a common question among TLA+ beginners. There can be bugs in the implementation. Those would either be bugs due to a mistranslation of the spec -- i.e., an error in the implementation -- or, because the spec also implicitly or explicitly describes the assumptions about the environment, a mismatch between the actual environment (hardware, software stack, user behavior) and the spec -- i.e. an error in the spe…
Comment linking /files/Trace.pdf
on “The Paxos Algorithm, or How to Win a Turing Award”Submitted The Best Programming Language (2017) as a story · 2 points
HN discussion
