5 ms·

I wrote some property-based tests for a parsing library. Eventually one of the tests for case-insensitive parsing failed... because it hit the letter "Ǆ" which

I wrote some property-based tests for a parsing library. Eventually one of the tests for case-insensitive parsing failed... because it hit the letter "Ǆ" which has upper, lower and title-case. The funny thing is that the parsing library was correct and it was the test property that was wrong—but I still learned about an edge case I had never considered! This has been a common pattern for "simpler" property-based tests I've written: I write a test, it fails right away, and it turns out that my code is fine, but my property was wrong. And this is almost always useful; if I write an incorrect property, it means that some assumption I had about my code is incorrect, so the exercise directly improves my conceptual model of whatever I'm doing.

nottorp 1y ago
That's Unicode, which has a whole section of hell dedicated to it.
- riwsky 1y ago
  Update: It’s actually been divided into multiple sections; if your code assumes a single section, it will break as of the addition of multibyte characters in Unicode v7.1
- atmavatar 1y ago
  When the robots rise up and exterminate the human race, Unicode will be one of the reasons we deserve it.
- rented_mule 1y ago
  Is the root of the problem Unicode? Or is the root of the problem the complexity of the union of written human languages? To the extent that it's the latter, Unicode is just the messenger.
  - nottorp 1y ago
    I would shed a tear but then I remember that they have not one, not two but four canonical forms... And what do they do about it? They add more emoji. Besides, even if it's justified, it's still sections 7.1-A to 7.3-D of hell.
testthetest 1y ago
Yes! We use a version of this in our end-to-end Playwright scripts as well, because we want our tests to be both: 1) lightweight, because most of our test suites run on production infrastructure and can’t afford to run them constantly 2) "creative", to find bugs we hadn’t considered before Probabilistic test scenarios allow us to increase the surface we're testing without needing to exhaustively test every scenario.
chriswarbo 1y ago
Indeed, I've had a property fail due to `Char.isWhitespace` disagreeing with a `\s` regex over whether Mongolian Vowel Separator counts as whitespace (it's not any more, but was prior to Unicode 6.3, according to https://unicode-explorer.com/c/180E https://unicode-explorer.com/c/180E ) It's been said (I think by Hughes?) that the causes of property failures tend to be spread equally between buggy code, buggy property and buggy generator.
senderista 1y ago
Yup, and many have discovered this is an unexpected benefit of formal methods in general: writing a formal spec forces you to think precisely about requirements, assumptions, and edge cases, independently of whatever benefit formal verification may provide.
sn9 1y ago
There are techniques to discover properties of your function as written, which can then tell you if you've written the function you intended to write: https://www.fuzzingbook.org/html/DynamicInvariants.html https://www.fuzzingbook.org/html/DynamicInvariants.html (also at https://www.debuggingbook.org/html/DynamicInvariants.html https://www.debuggingbook.org/html/DynamicInvariants.html)

nottorp 1y ago

That's Unicode, which has a whole section of hell dedicated to it.

riwsky 1y ago
Update: It’s actually been divided into multiple sections; if your code assumes a single section, it will break as of the addition of multibyte characters in Unicode v7.1
atmavatar 1y ago
When the robots rise up and exterminate the human race, Unicode will be one of the reasons we deserve it.
rented_mule 1y ago
Is the root of the problem Unicode? Or is the root of the problem the complexity of the union of written human languages? To the extent that it's the latter, Unicode is just the messenger.
- nottorp 1y ago
  I would shed a tear but then I remember that they have not one, not two but four canonical forms... And what do they do about it? They add more emoji. Besides, even if it's justified, it's still sections 7.1-A to 7.3-D of hell.

testthetest 1y ago

Yes! We use a version of this in our end-to-end Playwright scripts as well, because we want our tests to be both: 1) lightweight, because most of our test suites run on production infrastructure and can’t afford to run them constantly 2) "creative", to find bugs we hadn’t considered before Probabilistic test scenarios allow us to increase the surface we're testing without needing to exhaustively test every scenario.

chriswarbo 1y ago

Indeed, I've had a property fail due to `Char.isWhitespace` disagreeing with a `\s` regex over whether Mongolian Vowel Separator counts as whitespace (it's not any more, but was prior to Unicode 6.3, according to https://unicode-explorer.com/c/180E https://unicode-explorer.com/c/180E ) It's been said (I think by Hughes?) that the causes of property failures tend to be spread equally between buggy code, buggy property and buggy generator.

senderista 1y ago

Yup, and many have discovered this is an unexpected benefit of formal methods in general: writing a formal spec forces you to think precisely about requirements, assumptions, and edge cases, independently of whatever benefit formal verification may provide.

sn9 1y ago

There are techniques to discover properties of your function as written, which can then tell you if you've written the function you intended to write: https://www.fuzzingbook.org/html/DynamicInvariants.html https://www.fuzzingbook.org/html/DynamicInvariants.html (also at https://www.debuggingbook.org/html/DynamicInvariants.html https://www.debuggingbook.org/html/DynamicInvariants.html)