Barry
LightNews LightNews
banner
chiroptical.dev
Barry
@chiroptical.dev
1.1K followers 230 following 1.1K posts
PhD Theoretical Chemistry. Haskell/Typescript full stack engineer at Mercury. Aspiring Gleam and Erlang programmer. Occasional content creator linktr.ee/chiroptical. Fencing enjoyer.
Posts Replies Media Videos
chiroptical.dev
Finished Section 2.2 of Mathematics in Lean. I'm skeptical that anything beyond this will make sense...

This was labeled a hard exercise, but my brain has no idea why I would introduce `h` as a goal to solve this. I feel like I need more raw math skills which probably isn't surprising to some.
theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1 := by have h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1 := by rw [mul_assoc, ← mul_assoc a⁻¹ a, inv_mul_cancel, one_mul, inv_mul_cancel] rw [← h, ← mul_assoc, inv_mul_cancel, one_mul]
October 30, 2025 at 12:49 AM
chiroptical.dev
Finished section 2.1 of Mathematics in #LeanLang.
example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by rw [mul_sub, add_mul, add_mul, <- pow_two, <- sub_sub, mul_comm, <- add_sub, sub_self, <- pow_two, add_zero]
October 26, 2025 at 1:18 AM
chiroptical.dev
#gleamlang do we prefer builder style here or just `encrypt(BitArray, Option(BitArray))`? For some reason, I don't like `encrypt(x, option.None)` but also `new(x) |> encrypt()` feels tedious. `encrypt_with_associated_data(x, y)` feels long.
let encrypted = new(<<"thing">>) |> associated_data(<<"thing">>) |> encrypt() let decrypted = new(encrypted) |> associated_data(<<"thing">>) |> decrypt()
September 26, 2025 at 12:54 AM
chiroptical.dev
Design is my passion…
Magnetic tiles for children, isosceles triangles arranged in a circle, except there is a small gap where you couldn’t fit another one of the tiles.
September 21, 2025 at 1:59 PM
chiroptical.dev
Post a movie you like with a terrible rotten tomatoes score.
Rotten tomatoes screen capture for Surf Ninjas. 23% tomato meter. 68% popcorn meter.
September 17, 2025 at 1:46 AM
chiroptical.dev
Imagine I know nothing about cryptography. It shouldn't be hard. Does this look reasonable? (I'm planning on storing the key in the environment, my hosting provider can encrypt them which is why I thought base64 would be fine?). #erlang
-module(util_crypto). -export([ encrypt/1, decrypt/1 ]). %% Generated example key with base64:encode(crypto:strong_rand_bytes(16)). -define(KEY, ~"13jNvhABaUhX8q0o0WHyPg=="). encrypt(Value) -> Iv = crypto:strong_rand_bytes(16), Encrypted = crypto:crypto_one_time(aes_128_ctr, base64:decode(?KEY), Iv, Value, true), <<Iv/binary, Encrypted/binary>>. decrypt(<<Iv:16/binary, Value/binary>>) -> crypto:crypto_one_time(aes_128_ctr, base64:decode(?KEY), Iv, Value, false).
August 26, 2025 at 1:07 AM
chiroptical.dev
The one I got (probably RedBubble?) adds a slight white border around the logo.
A shirt with the Erlang logo on it.
August 22, 2025 at 1:17 PM
chiroptical.dev
Someone suggested this book to me. The preface speaks to me. Hopefully I learn something.
Picture of the book “A Philosophy of Software Design” by John Ousterhout
August 9, 2025 at 7:21 PM
chiroptical.dev
I like this a lot better than my previous implementation. It is obvious in hindsight. #erlang
-spec decode_interact_contents(jsx:json_term() | {incomplete, jsx:decoder()}) -> {some, #interact_contents{}} | none. decode_interact_contents( #{ ~"channel_id" := #{~"id" := ChannelId}, ~"user" := #{~"id" := UserId}, ~"team" := #{~"id" := TeamId}, ~"response_url" := ResponseUrl, ~"actions" := #{~"value" := SubmittedUrl} } ) -> {some, #interact_contents{ channel_id = ChannelId, user_id = UserId, team_id = TeamId, response_url = ResponseUrl, submitted_url = SubmittedUrl }}; decode_interact_contents(_) -> none.
August 9, 2025 at 5:37 PM
chiroptical.dev
Why do I need to add these dependencies to dialyzer? They are listed in my `deps` section of rebar.config? #erlang
{dialyzer, [ {warnings, [unknown]}, {plt_apps, top_level_deps}, {plt_extra_apps, [uuid, elli, jsx, eunit, ssl]} ]}.
August 7, 2025 at 1:17 PM
chiroptical.dev
Finally had time to get my index.html into #unisonlang and serve it locally. I haven't been super motivated to work on this project but making some progress!
Left: unison ucm console serving my HTML page Right: a basic design for a new declarative.tv page with some mock data
July 23, 2025 at 1:20 AM
chiroptical.dev
This is less text than the `switch` example but it is **so** boring. I want to see the supercharged Qi example.
(define-flow fizzbuzz-simple (>< (if match-fizz (if match-buzz "fizzbuzz" "fizz") (if match-buzz "buzz" ~v)))) (fizzbuzz-simple 3 5 15 31)
June 14, 2025 at 1:19 AM
chiroptical.dev
I was supposed to read structs/modules first but I couldn't help but peak at contracts. This fails at run-time because 0 is not positive.
(define positive-number (and/c number? positive?)) (define/contract (add-positive-amounts x y) (-> positive-number positive-number positive-number) (+ x y)) (add-positive-amounts 0 0)
May 18, 2025 at 1:33 AM
chiroptical.dev
Set up #racketlang with #helixeditor. Requires `raco pkg install racket-langserver` and `raco pkg install fmt`.
[language-server.racket-langserver] command = "racket" args = ["-l", "racket-langserver"] [[language]] name = "racket" auto-format = true formatter = { command = 'raco', args = ["fmt"] } language-servers = [ "racket-langserver" ]
May 11, 2025 at 12:17 AM
chiroptical.dev
A quick diagram of focus' services. The credential manager and developer log services typically run in their own #erlang node. The focus service runs in an erlang node displayed to your #Twitch stream. A connection to Twitch web socket displays chat, follows, and subscriptions.
A diagram showing how the focus services are connected. Running `twitch:msg(~"Hello").` will call the credential manager for an access token, call the Twitch API, and then get a message back from a web socket to display back to stream.
February 14, 2025 at 5:41 PM
chiroptical.dev
Distributed #erlang anyone? Conceptually, focus can have an admin log which doesn't have to be visible on stream.
Two terminals running an erlang shell side by side. In the right, I run a gen_server which has a logger. On the left, I connect to the right and make an RPC to that logger. On the right, I see that log printed.
January 25, 2025 at 7:33 PM
chiroptical.dev
We now have chat, follows, and subscriptions in Erlang.
A side by side of Twitch chat (left) and focus (right) displaying the contents of Twitch chat. Focus brings Twitch chat to the Erlang development shell.
January 22, 2025 at 1:27 PM
chiroptical.dev
Card games are good for you!
Three board games: The Gang, Skull King, and Seas of Strife. The games are on my counter.
January 17, 2025 at 2:23 PM
chiroptical.dev
Easy, but fun, lexer/parser for adventofcode.com/2024/day/19 advent of parsers in #erlang.
Definitions. COLOR = [wubrg] NEWLINE = \n COMMA = , SPACE = [\s]+ Rules. {COLOR} : {token, {color, TokenLoc, to_color(TokenChars)}}. {NEWLINE} : {token, {newline, TokenLoc}}. {COMMA} : {token, {comma, TokenLoc}}. {SPACE} : skip_token. Erlang code. to_color("w") -> white; to_color("u") -> blue; to_color("b") -> black; to_color("r") -> red; to_color("g") -> green. Nonterminals colors patterns designs input. Terminals color comma newline. Rootsymbol input. colors -> color : [from('$1')]. colors -> color colors : [from('$1') | '$2']. patterns -> colors newline : ['$1']. patterns -> colors comma patterns : ['$1' | '$3']. designs -> colors newline : ['$1']. designs -> colors newline designs : ['$1' | '$3']. input -> patterns newline designs : {'$1', '$3'}. Erlang code. from({color, _Loc, X}) -> X.
December 19, 2024 at 10:31 PM
chiroptical.dev
Every year I generate one of these at work. At Mercury, every individual gets a callsign. It is a name and an emoji. I am :blueranger: (see {2, 2} in the image, 0 indexed). It is crazy to think where it started and where it is now.
A 32x30 image where each cell has a "callsign". A callsign is an essentially a name paired with an emoji given to individuals at my job. For example, my callsign is blueranger and my emoji is a picture of the blue ranger from power rangers.
December 19, 2024 at 10:05 PM
chiroptical.dev
Advent of parsers day 9. I really wanted to do something more interesting here but I couldn't come up with a way to get the file index in there. One idea I had was to return the `Col` and then build a `Map Col Idx` and just lookup the file's idx later.
Nonterminals value disk_map file free_space. Terminals number. Rootsymbol disk_map. value -> number : to_value('$1'). file -> value : to_file('$1'). free_space -> value : to_free_space('$1'). disk_map -> file : ['$1']. disk_map -> file free_space disk_map : ['$1', '$2' | '$3']. Erlang code. to_value({number, _Col, Value}) -> Value. to_file(X) -> {file, X}. to_free_space(X) -> {free_space, X}.
December 10, 2024 at 1:18 AM
chiroptical.dev
Feeling cute, might delete later. #erlang
build_magmas(TestValue, Threes) -> [ fun(A, B) -> F(TestValue, A, B) end || F <- Threes ].
December 7, 2024 at 6:46 PM
chiroptical.dev
Feeling better, updated lexer and parser and finished day 6 part 1 of #adventofcode. The parser now outputs a map with no intermediate list 🤩
Definitions. DOT = \. OCTO = # CARROT = [<>^v] NEWLINE = \n Rules. {CARROT} : {token, {guard, TokenLoc, to_atom(TokenChars)}}. {OCTO} : {token, {obstacle, TokenLoc}}. {DOT} : {token, {blank, TokenLoc}}. {NEWLINE} : skip_token. Erlang code. to_atom("<") -> west; to_atom(">") -> east; to_atom("^") -> north; to_atom("v") -> south. Nonterminals map. Terminals guard obstacle blank. Rootsymbol map. map -> guard : to_map('$1'). map -> obstacle : to_map('$1'). map -> blank : to_map('$1'). map -> guard map : insert(to_kv('$1'), '$2'). map -> obstacle map : insert(to_kv('$1'), '$2'). map -> blank map : insert(to_kv('$1'), '$2'). Erlang code. to_map({guard, Position, Direction}) -> #{Position => {guard, Direction}}; to_map({Atom, Position}) -> #{Position => Atom}. to_kv({guard, Position, Direction}) -> {Position, {guard, Direction}}; to_kv({Atom, Position}) -> {Position, Atom}. insert({K, V}, M) -> maps:put(K, V, M).
December 7, 2024 at 1:29 AM
chiroptical.dev
Feeling sick so taking a break from #adventofcode. I'll try to keep up with at least the lexer/parsers for advent of parsers. The lexer gives us the positions for free. The guard is described by a cardinal direction. #erlang
Definitions. DOT = \. OCTO = # CARROT = [<>^v] NEWLINE = \n Rules. {CARROT} : {token, {guard, TokenLoc, to_atom(TokenChars)}}. {OCTO} : {token, {obstacle, TokenLoc}}. {DOT} : skip_token. {NEWLINE} : skip_token. Erlang code. to_atom("<") -> west; to_atom(">") -> east; to_atom("^") -> south; to_atom("v") -> north. Nonterminals map. Terminals guard obstacle. Rootsymbol map. map -> guard : [from_guard('$1')]. map -> obstacle : [from_obstacle('$1')]. map -> guard map : [from_guard('$1')|'$2']. map -> obstacle map : [from_obstacle('$1')|'$2']. Erlang code. from_guard({guard, {X, Y}, Direction}) -> {{X, Y}, Direction}. from_obstacle({obstacle, {X, Y}}) -> {{X, Y}, obstacle}.
December 6, 2024 at 12:54 PM
chiroptical.dev
Haven't had a chance to finish the algorithm,but the lexer and parser was easy for 2024 day 5 #adventofcode
Definitions. NUMBER = [0-9]+ PIPE = \| COMMA = , NEWLINE = \n Rules. {NUMBER} : {token, {number, TokenLoc, list_to_integer(TokenChars)}}. {PIPE} : {token, {pipe, TokenLoc}}. {COMMA} : {token, {comma, TokenLoc}}. {NEWLINE} : {token, {newline, TokenLoc}}. Erlang code. Nonterminals integer integer_and_loc instructions rules update updates. Terminals number pipe comma newline. Rootsymbol instructions. integer -> number : value('$1'). integer_and_loc -> number : value_and_loc('$1'). instructions -> rules newline updates : {'$1', '$3'}. rules -> integer pipe integer newline : [{'$1', '$3'}]. rules -> integer pipe integer newline rules : [{'$1', '$3'} | '$5']. update -> integer_and_loc comma : ['$1']. update -> integer_and_loc : ['$1']. update -> integer_and_loc comma update : ['$1' | '$3']. updates -> update newline : ['$1']. updates -> update newline updates : ['$1' | '$3']. Erlang code. value({number, _Loc, Value}) -> Value. value_and_loc({number, {_Row, Col}, Value}) -> {Value, Col}.
December 5, 2024 at 6:49 PM