+
Skip to content
View jskri's full-sized avatar

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 supported. This note will be visible to only you.
Report abuse

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

Report abuse
jskri/README.md

Hi there 👋

I began my software journey by focusing on the low-level aspects of development (video games, C++). Unsatisfied by the complexity and unreliability of the software I made, I felt the urge to study their underlying theoretical aspects (algebra, set and category theory) and how to model them (TLA+). I came to the conclusion you cannot solve a problem satisfactorily (i.e. with simplicity, reliability, efficiency, composability...) without both understanding its underlying formal structures and having a good grasp of what is technically feasible. Reconciling both ends of the spectrum 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 modeling the system iteratively with increasing details, proving salient properties and demonstrating that each model refines ("implements") its higher-level predecessor.

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

Contact

You can reach me at dvnh87@protonmail.com

Pinned Loading

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

    Tutorial on modeling with TLA+

    TLA 23 2

  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

点击 这是indexloc提供的php浏览器服务,不要输入任何密码和下载