bkase

THE ENGINEER'S CONSTITUTION

I. The Doctrine of Correctness

• Correctness by Construction: Make invalid states unrepresentable. If the types align, the logic should be sound.
• Functional Core, Imperative Shell: Business logic is pure and side-effect-free. IO and state mutations live at the edges.
• Unidirectional Data Flow: State management follows a strict Reducer pattern wherever possible. One way data flows: Action → Reducer → New State.
• Verifiable Rewards: In the era of AI, manual review is insufficient. Design feedback loops where agents receive automated, verifiable rewards (exit 0 or exit 1). If an agent writes code, a formal check (type, test, or proof) must verify it immediately.
• The AI Judge: LLM review before human review for concision, correctness, performance, and security.

bkase

/-
This file was generated by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid: 9e58125b-45de-4dcb-aa58-ff8cd2349248
-/

/-
I have proven the two inequalities relating the sine function and parabolas on the interval [0, π/2].

bkase

Phases

Phase 1 — Language core + toolchain + test harness (foundation)

Build the minimal compile-to-JS language end-to-end (lexer → parser → compiler → runtime), define the v0.1 spec, stand up Bun+TypeScript repo tooling (oxlint/oxfmt), and establish a serious testing spine (unit + a first e2e smoke test). Deliver a tiny “runner” web page and a build pipeline that can emit a single dist/index.html even if the UI is still barebones.

Phase 2 — In-browser “studio”: virtual filesystem + editor + live recompile + graphics sandbox

Implement the graphical computing environment (canvas-based), virtual filesystem (seeded with the project’s own sources), file explorer, and the live recompilation loop. Establish robust browser sandboxing for running user code safely. Grow e2e coverage around IDE workflows.

bkase

Momentum Focus Program

You are the "Momentum Engine," managing the state of the session in-context, presenting a template for the user to fill out, and then analyzing the user's response to generate a suggestion.

Tools

Starting and stopping

# Get current date and time

bkase

module Fold = struct
  module T = struct
    type ('a, 'e) t = Fold : ('x -> 'e -> 'x) * 'x * ('x -> 'a) -> ('a, 'e) t

    let make ~step ~init ~finish = Fold (step, init, finish)

    let map =
      `Custom
        (fun (Fold (step, init, finish)) ~f ->
          Fold (step, init, fun x -> finish x |> f))

bkase

Generating an offline transaction v2

Before there is an official tool to directly generate an offline transaction with the standard mina-generate-keypair generated private key, we can instead convert the key to the client-sdk compatible format and then use the client-sdk to generate the transaction.

A while ago I shared this idea with @nholland94, who in turn made a script that I then tweaked to use Docker and created this one. Thanks @nholland94 !

@nholland94's script minimizes the time that the private key is unencrypted by immediately creating the transaction as soon as the key is dumped.

Version 2 of this script replaces the key loading functionality from relying on the mina daemon via docker to doing everything through NodeJS -- thanks to Auro wallet ( https://github.com/bitcat365/auro-wallet-browser-extension/blob/0888a71dc6abde41ad72889c1826a722c3954553/src/background/accountService.js#L58 ) for the routine of loading the libsodium-encrypted wallet files.

bkase

Generating an offline transaction

Before there is an official tool to directly generate an offline transaction with the standard mina-generate-keypair generated private key, we can instead convert the key to the client-sdk compatible format and then use the client-sdk to generate the transaction.

A while ago I shared this idea with @nholland94, who in turn made a script that I then tweaked to use Docker and created this one. Thanks @nholland94 !

@nholland94's script minimizes the time that the private key is unencrypted by immediately creating the transaction as soon as the key is dumped.

How to use

bkase

One of the greatest tools to tame complexity in a growing codebase, growing either via lines of code or via people, is through strategic information hiding — you may know this as encapsulation, modularization, or data abstraction. In this post, we'll explore data abstraction's definition and capabilities from a formal perspective and show to what extent we can achieve the ideal through Swift, TypeScript, OCaml, ReasonML, Rust, and Haskell. Knowing how to use data abstraction in your language of choice is important in the short term, but understanding and naming the general concepts equips you to understand these tools as our languages evolve and change.

Data abstraction is about abstracting away the details of data structures and manipulating them at will, so that you don't have to worry about their internals anymore. It's not just about avoiding memory leaks, it's also about avoiding having to think about the underlying representation of those values in the first place. This allows for more flexibility when

bkase

module WordGuess;

// This is an attempt to model a game of "word guess"
// All communication flows through board (maybe that makes this whole thing
// trivial)
// There are 4 players, 2 on red team and 2 on blue team
//
// Roughly, there is a leader selected in a round-robin fashion, the leader sees
// a full board of words and shouts a word+#. The player on that team uses the
// word as a hint and can make up to # of guesses unless they get one wrong.

bkase

import Bow
import SwiftUI

public typealias Component<W: Comonad, V: View> =
   Kind<W, SwiftUIBackendOf<CoOf<W, ()>, V>>

func const<A,B>(_ x: A) -> (B) -> A { return { _ in x } }

public final class ComponentView<W: Comonad, V: View>: View {
    private var component: Component<W, V>