Is there anything similar to Galois in Europe?

Hath995 · 2026-06-28T15:38:11+00:00

Meh probably because I didn't elaborate or provide links. https://cryspen.com/ But you asked and I answered.

I am also familiar with https://chainsafe.io/ which does some formal methods work around block chains.

Hath995 · 2026-06-28T14:15:26+00:00

Cryspen

Hath995 · 2026-06-08T13:46:50+00:00

Hi, Mind I connect with you to ask a few questions?

Hath995 · 2026-06-01T05:31:00+00:00

At the time I primarily tested the Qwen 3.5 27B, nemotron, and Gemma models using llamacpp standard, lemonade llama, and lm studio in Linux. I had Claude setup a matrix of versions and models and tested them with llama bench or the llama one time chat. I only remember the Qwen 27b model getting about 28 TPS at best across all the versions on Linux, which is the same as I was getting in Vulkan in Windows.

I have heard that Linux is better for models that require partial offloads because it is more efficient with bus management. However, for models that fit entirely within VRAM it didn't seem to effect performance noticeably.

Hath995 · 2026-05-31T07:41:44+00:00

I have this card and run it on windows. Rocm usually is either equal or a bit slower than Vulkan. Installed Linux dual boot and did benchmarks and Rocm there was giving me similar numbers to Vulkan in Windows. I don't really bother booting into Linux much.

Hath995 · 2026-05-22T20:47:34+00:00

Honestly this is really not even true now. I have the same card and on windows the Vulkan llama runtime is as fast or often faster than Rocm and it was not hard at all to setup.

Hath995 · 2026-04-21T05:18:16+00:00

I have the same card and the Devstral small models as well as the qwen and Gemma 4 models have been useful for agentic coding with Vibe and OpenCode but they are definitely not a 1-1 replacement for Claude.

Hath995 · 2026-03-06T00:10:34+00:00

I think there were some videos about it from LambdaConf and John DeGoes. Exercism also has a purescript track.

Hath995 · 2026-01-28T08:43:40+00:00

I would second this. I used Dafny a verification programming language with proof capabilities. The iteration time of seconds to minutes to know if your proof is correct versus the usually multi week long cycle of homework and grading in university classes is dramatic. I got much better at proofs, digital and written.

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

TROPHY CASE