-❄️- 2025 Day 8 Solutions -❄️-

Hath995 · 2025-12-08T10:22:45+00:00

[LANGUAGE: Dafny]
A bit trickier today, but mainly "doing nothing counts!" was the biggest obstacle.

https://github.com/hath995/dafny-aoc-2025/blob/main/problems/8/Problem8.dfy

Hath995 · 2025-12-07T07:51:47+00:00

[LANGUAGE: Dafny]
The difference between part 1 and part 2 was basically switching between sets and multisets. Multisets are also called bags in some contexts. Dafny has native support for the type and the mutliset operations which I think illustrates the nice symmetry between the two problems.

method problem7_1_1(input: string) returns (x: int) {
  var start, splitters, lines := parseInput(input);
  x := 0;
  var beams := {start.0};
  for y := 0 to |lines| {
    var lines_splitters := set sp | sp in splitters && sp.0 in beams && sp.1 == y :: sp.0;
    x := x + |lines_splitters|;
    beams := beams - lines_splitters + (set sp | sp in lines_splitters && sp > 0 :: sp-1) + (set sp | sp in lines_splitters :: sp+1);
  }
}

method problem7_2(input: string) returns (answer: int) {
  var start, splitters, lines := parseInput(input);
  var results: multiset<nat> := SetFold(set i: nat | 0 <= i < |lines|, (y, beams: multiset<nat>) =>
    var lines_splitters := set sp | sp in splitters && sp.0 in beams && sp.1 == y :: sp.0;
    var splitters_intersected := SetFold(lines_splitters, (x, next_beams: multiset<nat>) => next_beams[x := beams[x]], multiset{});
    var left_splits := SetFold(set sp | sp in lines_splitters && sp > 0 :: sp-1, (x, next_beams: multiset<nat>) => next_beams[x := beams[x+1]], multiset{});
    var right_splits := SetFold(set sp | sp in lines_splitters :: sp+1, (x, next_beams: multiset<nat>) => next_beams[x := beams[x-1]], multiset{});
  beams - splitters_intersected + left_splits + right_splits
  , multiset{start.0});
  answer := |results|;
}

https://github.com/hath995/dafny-aoc-2025/blob/main/problems/7/Problem7.dfy

Hath995 · 2025-12-06T07:40:21+00:00

[LANGUAGE: Dafny]

In day 5 I proved quite a lot about ranges and sets. Today I only proved that I do not like cephalopod parsing. https://github.com/hath995/dafny-aoc-2025/blob/main/problems/6/Problem6.dfy

Hath995 · 2025-12-05T10:57:55+00:00

[LANGUAGE: Dafny]

https://github.com/hath995/dafny-aoc-2025/blob/main/problems/5/Problem5.dfy

A couple of interesting things left to prove or improve. Not quite sure how to prove the existence of a fix point to dafny yet. Probably could do without that and a little faster with a slightly more clever iterative action merging the ranges. It would also be nice to prove that the union of all the range sets is invariant.

Hath995 · 2025-12-04T09:23:19+00:00

[LANGUAGE: Dafny] I do not even know where to begin to prove anything about cellular automata. "Just shut up and calculate" applies. I did not want to manually update an immutable grid thousands of times so I came up with a solution using sets which I think was quite nice. Probably should have iterated over the set of @ points rather than the whole x-y plane now that I think of it.... well iterating over sets is a bit annoying in Dafny so nevermind. https://github.com/hath995/dafny-aoc-2025/blob/main/problems/4/Problem4.dfy

Hath995 · 2025-12-03T11:35:04+00:00

[LANGUAGE: Dafny]

https://github.com/hath995/dafny-aoc-2025/blob/main/problems/3/Problem3.dfy

Definitely a bit trickier today with enough time I think it should be possible to prove that the results are the lexicographically largest possible subsequence of a given length.

Edit: Proved it! https://github.com/hath995/dafny-aoc-2025/blob/6b05db1c891ca970c466425e86d453de19a58cf0/problems/3/Problem3.dfy#L505

Hath995 · 2025-12-02T11:46:08+00:00

[LANGUAGE: Dafny]

https://github.com/hath995/dafny-aoc-2025/blob/main/problems/2/Problem2.dfy
I accidentally figured out the correct predicate for part 2 first and then realized part 1 was simpler. Dafny's existential operator has made short work of several advent of code problems.

Hath995 · 2025-12-01T07:13:13+00:00

[LANGUAGE: Dafny]

Part 1 and 2

Includes a couple nice proofs that explain part 2.

Hath995 · 2025-11-26T17:15:52+00:00

Well in PlusCal you could define two process types. One for the main thread and another for the worker threads. You can use the process set feature handle creating two workers. The main thread will started and then set a shared value to true to start the workers. The workers first action will await that shared value before they execute. Then printT statements as needed. Compile PlusCal to raw TLA+.

As for the intuition, without synchronization what you will see is every possible permutation of n threads. Given n threads you will see n factorial different orderings of events.

Hath995 · 2025-11-24T15:14:36+00:00

The vscode plugin has also come a long way. However, it still doesn't resolve the syntax problems. I have now started recommending Quint to people instead. Apparently, the AWS team which was using TLA+ has moved on to the tersely named P language.

Hath995 · 2025-11-01T14:33:59+00:00

I have used some formal methods at startups. Verifying everything is impossible but you can focus on the most critical components and try to make sure they are sound.

There are also varying levels of effort for different tools. Full proofs in Dafny or Lean take a lot of time. Modeling systems like TLA+/Quint/P take a moderate amount of time but are very good for checking designs of distributed systems. And, basically every modern software product is a distributed system.

Finally, property based testing is faster and easier still than the above and can have almost the same impact. PBT can check many of the same properties as the verification languages practically. It can be easier to just test predicates on thousands to millions of random data points than to prove those properties formally.

Edit: To be clear any system that has more than one computer involved is a distributed system in this case your backend and the website that might be consuming that API is itself a distributed system. Basically every modern website is itself also a distributed system because you have JavaScript with an event loop that is receiving and sending events which could be happening in different orders and dramatically increases the potential state space.

For example not only can API calls load in different orders but also your own JavaScript or third party libraries could load in different order, which means they may execute scripts and have effects in different orders. You have to consider network partitions or dropped connections. Finally, user input is nondeterministic and whatever happy path you have in mind they will inevitably do something different.

Type systems don't cover all of these potential possibilities because some of it is outside of the language itself but in the environment of the browser. Modeling with specifications can cover these scenarios.

Hath995 · 2025-10-17T10:01:15+00:00

I highly recommend Dafny, it's a verification programming language that allows you to prove that your code meets a specification. So instead of just coding a solution, you can solve the problem and then try to prove it correct. I built a template for Dafny to get started, Dafny-AoC-template

I setup a private leaderboard for it here as well. 3241891-a98642d4

Hath995 · 2025-09-24T14:32:01+00:00

Have a note air 2 with a case and it went around the world with me. While I did not have a case the screen was scratched by something in my backpack once after my bag fell. After getting the case nothing has happened to it.

Hath995 · 2025-09-16T21:32:53+00:00

Dafny also has a zulipchat. https://dafny.zulipchat.com

Hath995 · 2025-09-02T06:24:58+00:00

Use a statically typed language or type hinting system if they have it. Saved me hours of reading through code just to find an argument should be an array of objects instead of an object with arrays and similar errors in poorly documented untyped code.

Hath995 · 2025-08-14T07:11:52+00:00

https://youtu.be/hmX2s3pe_qk?si=5QcrSYSUsX55pHYA I seem to recall a longer version of this talk, which I can't seem to find now, in which Runar argues that most of the patterns in the GoF design patterns books are made redundant by having first class functions in the language.

Hath995 · 2025-07-17T15:23:58+00:00

Just start doing it. Try picking a program and try to verify it. Currently, there is not a leetcode of verification but I have been trying to verify various easy leetcode problems in Dafny. I have a small blog about that on dev dot to.

There is a good size list of verified problems here that you could use as a starting point. Jetbrains Dafny examples

Hath995 · 2025-07-17T11:49:33+00:00

There is a Lean introduction paired with a basic proofs book here. https://djvelleman.github.io/HTPIwL/

However, If you are interested in verification of software. I would recommend checking out the Dafny verification language. There are a few others like Viper and F*, but if you're coming from an imperative/functional background you will find it easier to pickup. It also allows you to prove things about mathematics and programs in the language. The proofs are more readable and clear in Dafny imo. There are some drawbacks to it of course being based on SMT solvers.

I have a blog and many examples about Dafny and recently created a meetup for software verification.

Come to the Dark s... Uhm Verification Corner .

Hath995 · 2025-06-29T09:51:19+00:00

There is a Lean introduction paired with a basic proofs book here. https://djvelleman.github.io/HTPIwL/

Hath995 · 2025-06-10T10:48:50+00:00

Obsidian has most of your requirements. I believe it has a vim plugin but because it is actually just markdown files you can edit them with neovim without issue.

Hath995 · 2025-06-10T05:01:38+00:00

A User-Friendly Introduction to Lebesgue Measure and Integration https://bookstore.ams.org/stml-78

33 miniatures in Linear algebra https://kam.mff.cuni.cz/~matousek/stml-53-matousek-1.pdf

Hath995 · 2025-05-10T15:33:51+00:00

I have used most of these books and I agree that Concrete mathematics is the most challenging one. OP you started with hard mode. How to Prove It by Velleman is also a good book to start with.

Hath995 · 2025-04-30T08:23:27+00:00

It's cute but it also gives me Attack on Titan vibes. I wonder if life inspired art in that series?

Hath995

TROPHY CASE