[HN Gopher] Modelling the archetype of a message-passing bug wit...
       ___________________________________________________________________
        
       Modelling the archetype of a message-passing bug with TLA+ (2022)
        
       Author : surprisetalk
       Score  : 27 points
       Date   : 2024-09-15 16:33 UTC (4 days ago)
        
 (HTM) web link (medium.com)
 (TXT) w3m dump (medium.com)
        
       | dboreham wrote:
       | If only TLA+ could work with the actual product code, or even
       | some machine-translation of same.
        
         | dmytroi wrote:
         | Then it will be too noisy or too slow to be useful due to too
         | many intermediate states. The feature of TLA+ is that it forces
         | you to greatly dumb down the code to be able to use it, so it's
         | more of verifying an algorithm represented as visual graph
         | blocks rather than verifying assembly instructions.
         | 
         | I understand the wish for a magic bullet to just verify already
         | existing code, but I recon the answer to this is to verify code
         | before it's even written.
        
           | dboreham wrote:
           | Hmm well obviously I know this, and it's like that because
           | doing it properly is so far unachievable. Problem is there's
           | an uncontrolled step between the code being run and the code
           | being verified. This means we only verify an artist's sketch
           | of the thing we want to test.
        
       ___________________________________________________________________
       (page generated 2024-09-19 23:01 UTC)