Statistics Library Blog by Bhaveshb-bytes · Pull Request #43 · dafny-lang/blog

Bhaveshb-bytes · 2025-12-05T18:40:27Z

This serves as the PR for the blog post for official Statistics Library. @robin-aws Please let us know if there are any changes needed on the content or the CI side

This reverts commit 96d1888.

robin-aws

Very nice work on this, very readable and does a great job motivating the contribution and describing the journey to the final product.

robin-aws · 2025-12-08T20:27:05Z

+
+## Order statistics: median and range
+
+Beyond mean and variance, a statistics library should also provide basic order statistics such as median and range. Since Dafny’s standard collections already provide a merge sort ([MergeSortBy](https://github.com/dafny-lang/dafny/blob/68fb5ed04006b9be9601695d3d74687bbe3800b4/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy#L1041)), we reuse it rather than re–implement ordering ourselves . This is exactly the kind of situation where strong libraries make a difference: instead of proving sorting correctness again, we can build directly on a verified component and focus on the statistical logic itself.


robin-aws · 2025-12-08T20:28:08Z

+  }
+{% endhighlight %}
+
+You remember our first line, What looks simple in code often becomes interesting the moment you try to prove it. This is one of the cases where we faced such an issue. Our FrequencyTable function seemed simple: take a sequence and build a map counting occurrences.


Suggested change

You remember our first line, What looks simple in code often becomes interesting the moment you try to prove it. This is one of the cases where we faced such an issue. Our FrequencyTable function seemed simple: take a sequence and build a map counting occurrences.

You remember our first line: "What looks simple in code often becomes interesting the moment you try to prove it." This is one of the cases where we faced such an issue. Our FrequencyTable function seemed simple: take a sequence and build a map counting occurrences.

Made the required changes

robin-aws · 2025-12-08T20:28:23Z

+{% endhighlight %}
+
+You remember our first line, What looks simple in code often becomes interesting the moment you try to prove it. This is one of the cases where we faced such an issue. Our FrequencyTable function seemed simple: take a sequence and build a map counting occurrences.
+Now , Formally, we wanted Dafny to verify:


"Formally" as in previously?

'Formally' was a bit ambiguous there. I have rephrased the sentence to: 'To ensure correctness, we formally had to verify that:' to make the intent clearer.

robin-aws · 2025-12-08T20:39:41Z

+{% endhighlight %}
+
+This design has a few advantages:
+- It runs in *O(n)* time: one pass to build the frequency map and one pass to find the best.


This is a bit too strong a claim, for two different reasons:

Building the frequency table actually takes quadratic time because each map update such as m[key := m[key] + 1] have to make a new copy of the map (since Dafny maps are immutable). This could be optimized in the Dafny runtimes but hasn't been yet.

Each map lookup is not necessarily constant time in practice, because the runtimes generally use something like a HashMap, which is only going to be constant time on average, but can be linear in the worst case.

The first point could hypothetically be addressed by using a MutableMap from the Concurrent standard library, but the second point is a pretty fundamental data structures limit.

You definitely don't need to address this in the library itself, but you may want to add a bit of this detail, and definitely soften this runtime claim. It's still definitely true that the original version was quite a bit worse than quadratic :)

I agree with the points. Writing Linear time is sort of a tall claim and hence, I have made the required change here by telling how our approach is better.

robin-aws · 2025-12-08T20:44:22Z

+They also show how simple it is to work with the module: you can call Mean, Median, VariancePopulation, Mode, and the rest just like any normal function without worrying about the underlying proofs. In that sense, the tests double as a quick “how to use this library” guide while demonstrating its correctness on real data.
+
+
+## Acknowledgments


Consider swapping the last two sections, I think it flows a bit better to end with acknowledgements

robin-aws · 2025-12-08T20:47:54Z

+layout: post
+title:  "A Verified Statistics Library for Dafny"
+author: Bhavesh Bhatia and Tanay Mathur
+date:   2025-12-01 09:00:00 +0000


Just FYI since it came up earlier, this date is only used to allow blog posts to be merged that should not be actually published until a future date. When this is merged, as long as this date is in the past the new post will appear with the correct actual publication date. In other words this value is just fine. :)

robin-aws · 2025-12-08T20:59:29Z

+Because our helper `SumSquaredDifferences` is proven non-negative, Dafny automatically verifies that `VariancePopulation` and `VarianceSample` are also non-negative. Note that `VarianceSample` requires `|s| > 1`, because dividing by N - 1 where N is 1 would cause a division by zero!
+
+### 5. Standard Deviation
+ Finally, we arrive at Standard Deviation, which is the square root of the Variance. Since Dafny doesn't have a built-in square root, we define an `extern` function in a separate module.


Dafny doesn't have a built-in square root

Actually it does now! A new floating point type was added that supports square root: https://dafny.org/dafny/DafnyRef/DafnyRef#5236-mathematical-functions

You can just rephrase this to say it didn't have this at the time, and perhaps mention in the future work section that we could refactor the code to use this new type, and hence make it no longer target-specific.

Ah! Thank you for letting us know. I have added the point as you asked me to!

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Reworded sections for clarity and improved flow. Added acknowledgments section back to the document.

Corrected phrasing for clarity regarding Dafny's capabilities.

Bhavesh Bhatia and others added 12 commits December 2, 2025 00:13

Initial version

d40722b

Some changes

af4fd85

Changes in blog post for Std.Statistics library

41f5be5

Final blog

96a1666

cleanup

a107b1a

cleanup

3e85c88

cleanup

60efa28

cleanup

4003650

Name change for file

96d1888

Revert "Name change for file"

f22c4d7

This reverts commit 96d1888.

Name change for file

021da1a

removal of old file

18987e5

robin-aws requested changes Dec 8, 2025

View reviewed changes

robin-aws reviewed Dec 8, 2025

View reviewed changes

Tanay261 and others added 5 commits December 8, 2025 18:45

Update _posts/2025-12-01-statistics-library.markdown

b2d0ebe

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Update _posts/2025-12-01-statistics-library.markdown

e4c905e

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Updating statistics blog

e181c85

Reworded sections for clarity and improved flow. Added acknowledgments section back to the document.

Updating statistics blog

b74be07

Corrected phrasing for clarity regarding Dafny's capabilities.

mode point updation

4b92f5e

Bhaveshb-bytes requested a review from robin-aws December 9, 2025 13:45

Merge branch 'main' into main

c9ab1fa

robin-aws approved these changes Dec 9, 2025

View reviewed changes

keyboardDrummer approved these changes Dec 10, 2025

View reviewed changes

keyboardDrummer merged commit 15b9ed0 into dafny-lang:main Dec 10, 2025
1 check passed


		## Order statistics: median and range

		Beyond mean and variance, a statistics library should also provide basic order statistics such as median and range. Since Dafny’s standard collections already provide a merge sort ([MergeSortBy](https://github.com/dafny-lang/dafny/blob/68fb5ed04006b9be9601695d3d74687bbe3800b4/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy#L1041)), we reuse it rather than re–implement ordering ourselves . This is exactly the kind of situation where strong libraries make a difference: instead of proving sorting correctness again, we can build directly on a verified component and focus on the statistical logic itself.

	You remember our first line, What looks simple in code often becomes interesting the moment you try to prove it. This is one of the cases where we faced such an issue. Our FrequencyTable function seemed simple: take a sequence and build a map counting occurrences.
	You remember our first line: "What looks simple in code often becomes interesting the moment you try to prove it." This is one of the cases where we faced such an issue. Our FrequencyTable function seemed simple: take a sequence and build a map counting occurrences.

		They also show how simple it is to work with the module: you can call Mean, Median, VariancePopulation, Mode, and the rest just like any normal function without worrying about the underlying proofs. In that sense, the tests double as a quick “how to use this library” guide while demonstrating its correctness on real data.


		## Acknowledgments

Uh oh!

Conversation

Bhaveshb-bytes commented Dec 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

robin-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Bhaveshb-bytes commented Dec 5, 2025 •

edited

Loading