3 ms·
In the real world, many of us don't have the time to create formal proofs. But our instinct in testing where edge cases may exist in code that we wrote is a typ
by noduerme 5mo ago
In the real world, many of us don't have the time to create formal proofs. But our instinct in testing where edge cases may exist in code that we wrote is a type of refactoring that happens in our brains during the coding process. Hand the coding off to a machine and you have no idea where to start looking for the flaws.
- bluGill 5mo ago> Hand the coding off to a machine and you have no idea where to start looking for the flaws. I have found this quickly becomes false. I have learned I cannot review llm generated code as if it is written by a trusted senior developer (where I often just do a quick look, see nothing obvious and hit approve). Once you start reading the code in depth with the goal of understanding you quickly see the places where flaws are likely. Sure I start with no clue where to look, but it doesn't take long to see things.
- noduerme 5mo agoYes but it takes much longer to trace them. Because the LLM code almost always gravitates toward data blobs and highly dynamic objects and spaghetti that takes a ton of cognitive load to understand what their failure modes are. Even when it does document them.
- teiferer 5mo ago> In the real world, many of us don't have the time to create formal proofs Of course not. That's why they are so rare. But I thought we live in an AI era now where this kind of stuff can be done by a machine.