Skip to content
View jskri's full-sized avatar
4 followers · 0 following

Achievements

Achievement: StarstruckAchievement: Pull Shark

Achievements

Achievement: StarstruckAchievement: Pull Shark

Block or report jskri

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
jskri/README.md

Hi there 👋

I came to software through low-level development, with more than 10 years of C++ (video games and related systems). Unsatisfied by the complexity and unreliability of the software I wrote, I felt the urge to explore the theoretical foundations behind it: algebra, set theory, category theory, and formal modelling tools (TLA+, Coq/Rocq). I came to the conclusion that no problem can be solved satisfactorily, in terms of simplicity, reliability, efficiency and composability, without both understanding its underlying formal structures and having a good grasp of what is technically feasible. Reconciling theory and practice is what I find fascinating about this field.

Sources of inspiration

  • I like the correct-by-construction approach, as explained in the article Faultless systems: yes we can!. This involves modelling the system iteratively with increasing detail, proving key properties and proving that each model refines ("implements") the higher-level model.

  • I also find the work of Conal Elliott inspiring, for its emphasis on simplicity and composability.

Contact

You can reach me at jskri@proton.me

Pinned Loading

  1. modeling-with-tla modeling-with-tla Public

    Tutorial on modeling with TLA+

    TLA 24 3

  2. categorical-circuits-of-components categorical-circuits-of-components Public

    Defines circuits of components and their algebraic optimisation, based on categorical constructions such as compact closed categories.

    Lua

  3. controlling-cars-on-a-bridge controlling-cars-on-a-bridge Public

    TLA 1

  4. lets-prove-leftpad lets-prove-leftpad Public

    Forked from hwayne/lets-prove-leftpad

    Proving leftpad correct two-dozen different ways

    SystemVerilog