I’ve been studying Formal Methods again since the beggining of this year, and now I’m looking at algebraic specifications and I found they pretty elegant. To be able to pratice with it I vibecoded an algebraic specification plugin for Claude, and named it algae . Since I more interested into understanding the proofs I’m focusing on a syntax that make everything explicit, instead of focusing on…
(AI Generated) Formal specification has a reputation problem. People hear “model checking” and think avionics, nuclear reactors, safety-critical systems with million-dollar budgets. The implicit message: if nobody dies when your code breaks, you don’t need it. That’s wrong. Formal specifications add value to any project where you need to reason about behavior — which is most projects. Caelum is an…
(AI Generated) What if you could prove that your Perl function is correct — not just test it with a few examples, but mathematically verify that it satisfies its specification for all valid inputs? That’s what perlchecker does. perlchecker is a Rust tool that formally verifies annotated Perl functions using symbolic execution and SMT solving (Z3). You write preconditions and postconditions as…
I’ve been work in a project that requires installation of a huge amount of packages during testing. I usually setup the upstream repostiories, the problem with this is that it keep downloading the same package again and again and a lot of time and network bandwith could be saved if the packages were cached locally. Today I decided to spend some minutes looking into how to do it with nginx. And it…
Meat author: Yes, this post was generated mostly by GPT5, but I’m adding my own notes to make things clearer and funnier. Soo all italic stuff is me (an human) “speaking” Summing up I was trying to get a SDL3 hello world working, I fell alone and what ppl do when they fell alone? Yes, they write indie games, so do I. So I (as most developers in 2025) went to GPT and asked for a SDL3 hello world,…
Large Language Models (LLMs) are great at responding to prompts, but what if you could orchestrate multiple LLMs to collaborate, each playing a specific role, like characters in a game or components in a system? That’s exactly what I explored with a tool I developed using LangChain and Ollama , two fantastic libraries that make it easy to run local LLMs and compose them into complex chains. The…
Generic programming in C++ often requires carrying type information through function signatures or data structures. This can complicate interfaces and usage when the exact types are not known at compile time or when they vary. One common challenge is how to write code that can accept and operate on heterogeneous types without exposing those types explicitly to every caller. This blog post explains…
Leveraging C++ Phantom Types for Enhanced Type Safety Hey there, it’s me again, diving into another C++ gem that can make your code safer and more expressive. Today, I’m talking about phantom types , a nifty technique to enforce type constraints at compile time without any runtime cost. If you’re a fan of catching errors early (like I am), you’ll love how phantom types can prevent entire classes…
In this post I explain how I used fuzz testing to catch bugs in a date time parsing library I’m contributing to. Fuzz testing means testing some system with random input data and iterate over mutations of that input data in order to find inputs that drive the testing code to a bug, crash or similar. As I said I’m contributing to a date parsing library uutils/parse_datetime writen in Rust in order…
In this post I show why I would chose Rust over other languages for a project in present date. I do this by using a library for parsing dates as example, exposing strong points of Rust in a real example instead of speaking abstractly. Before starting let me state the problem properly: We want to parse strings into dates. The strings will be assumed to be a list of data elements separated by…
Sometime ago I started working with React again and after some few weeks I already had one of that components with dozens of useState calls. At that point I learned useReducer hook (I already used Redux before but never this hook). In this post I show how I write components with useReducer as state machines and how this make it more predictable and easier to manage the state updates. useReducer is…
Something that I think is realy useful when working with abstract syntax trees, is the possibility to do tree transformations. Trees transaformations can be used to add information to the AST from a semantic analysis, add positions, do optimizations, inline functions, etc. In this post I show what I learned after trying to achieve good tree transformations API in my code. First things first: I’m…
I was wondering if it would be possible to implement infinite recursion (TCO) in Python by using exceptions to discard the intermediary stack frames, and IT IS POSSIBLE! Here is how, more explanation after the code class Unwind ( Exception ): def __init__ ( self , * args , ** kwargs ): self . args = args self . kwargs = kwargs def tco ( f ): unwind = False def _inner ( * args , ** kwargs ):…
Is possible to encode dependent pairs (or sigma types) in python using TypeGuard , abtract classes and subtyping. Dependent pair is a pair of a value and a predicate about that value, in Coq is denoted like this (x : { n : T, P n }) , where T is a type and P is a predicate. Using abstract classes, subtyping and type guards is possible to achieve dependent pairs, here is an example: from abc import…
I was playing with a simple ML like grammar in the past weeks involving algebraic data types at the form data <type> = <ctr> <arg0> ... <argn> | ... I got me asking myself if it would be possible to compile this to Scott encoding so that we have only functions at evaluation time. I will use option type as example here: data option = some x | none and match expressions as eliminators match x with |…
call/cc is an Scheme function that make it possible to implement all sorts of control flows. From loops to generators, try/catch, green threads, etc. In this post I show a simple implementation of call/cc and talk a little about small-steps semantics. The whole code can be found here Small-step semantics When you’re implementing a interpreter that are some ways to do it. The most intuitive way is…
In this post I evolve the idea of typechecking Python code by using the ast module introduced at Polymorphic Typechecking in Python by Unification , but instead of using unification I use evaluation to compare the types. The code that we will typecheck can be found here and the typechecker here . To run the typechecker and the tests clone the repo and do this: # running the typechecker python…
In this series of posts I will port this post about dependent typed lambda calculus to Python. This is the third and last one Dependent typed lambda calculus (with tests) . I continue from where I stopped in the second one: Simply typed lambda calculus in Python In comparison with the simply typed version the code changed little, I dropped the mini parser because it would be too complicated to…
In this series of posts I will port this post about dependent typed lambda calculus to Python. This is the first type : Untyped lambda calculus (with tests). This code uses functions implemented/explained in the Functional programming in Python post so you man want to reference it. Untyped lambda calculus in Python import re from typing import * from fphack import pipefy , pipefy_builtins ,…
In this series of posts I will port this post about dependent typed lambda calculus to Python. This is the second one Simply typed lambda calculus (with tests) . I continue from where I stopped in the first one: Untyped lambda calculus in Python All the code can be found here : https://github.com/dhilst/lampy3/blob/master/stlc.py In this one I had to use a simple parser for the types, to make it…
While trying functional programming in Python there are two things that I think always come as pain points. The first, chaining or composing functions. The second is the error handling composition. In this post I how implement an usable pipe operator how to get most of the functions with partial application and an ExceptionMonad to abstract try/catchs. Pipe operator In OCaml we have the pipe…
In the Simple Python typecheker in Python I show how to bootstrap a simple typecheker in Python using the ast module. In this post I continue the saga adding parametric polymorphism a lá SML. To attach information to the functions I will use a sig function. This function does nothing in runtime and receives a constant string as argument from where we take the typing information. Here is the code…
In this post I will show how to implement a show function in OCaml with GADts and existentials and how to recover/implement dynamic dispatch in OCaml. I’ve been working with OCaml in the last months. It’s a wonderful language, fully functional with opt-in imperative features. But one thing that I miss is things being printable by default. In Haskell we have the show function that works almost…
Here is how to bootstrap a simple Python typechecker in Python. The idea is using the ast module of Python to parse some code into a typed AST and then traverse the AST checking the types. In this example I will type check function calls only, to do this the functions being called need to be annotated. Here is the code that we will typecheck def inc ( a : int , b : int ) -> int : return a + 1 def…
What you can do only with functions? In this post I will show a small implementation of a LISP like interpreter where it has no data structures, only functions, and show some examples of how to get recursion with anonymous functions and lists with it. First things first, the implementation is here: https://github.com/dhilst/lis.py It’s an small LISP like interpreter wrote in Python using only the…
I’m a big fan of ADTs (algebraic data types or sum types) because they make so easy to model stuff. You split your data in cases and then do case analysis functions to determine what to do. It’s possible to encode ADT with objects but it’s bloatted in someway, for example the Maybe datatype: data Maybe a = Just a | None may be encoded as: from dataclasses import dataclass class Maybe : pass class…
On LISP world is well known that functions and data are not so distinct entities. Every LISP program is data and code, at the same time. Other place where this happens is in lambda calculus, where you have only functions, (closures to be more precise), and it’s still possible to encode data structures. In this post I will talk about Scott Encoding and show how it works. We can encoding arbitrary…
I always wondered how it would be to use a function that application is right associative. I mean, instead of calling functions like this f(x) or f x we can call it like this x f , basically the call is inverted you have the arguments first then the function. And what would be the implications of this change. The pipe operator is known in OCaml for providing something like that, so foo |> bar is…
CPS + Curry + Pipe Operator in Python, this what FP can do for you Before begin I would like to alert that there is no AST manipulation here. These are just functions returning functions, calling and being called. The only class in this code is to make use of >> operator as a pipe operator, but any other operation would because this is simply function transformations. WTF is CPS? First let me…
C# has reference and value types. Reference types defaults to null but value types has each one it’s own default. If you have the type in hand you can generate a default with defaul(T) or usully just default . The problems with value defaults are they are anoying when you’re dealing with APIs and databases. Before going further let’me explain. PS: I’ll be talking a lot of extension methods if you…
You can use phatom types to secure your API, creating type safe indentifiers (like ints or strings). dotnet will not erase phaton types, so you will endup with a boxed type for a primitive, anyway is a cool trick to have on sleave. Here is how: namespace lsharp { // This is a "typed int" you can use with a type parameter // to explicify what "type of int" this would be. This is // particularly…
Here is how to creating a Postgres database in memory for testing! On your docker-compose replace the volume folder by a tmpfs entry, and you’re done. diff --git a/src/docker-compose-dev.yml b/src/docker-compose-dev.yml index ead4090..7a10881 100644 --- a/src/docker-compose-dev.yml +++ b/src/docker-compose-dev.yml @@ -82,4 +82,5 @@ services: volumes: - - pg_dbdata:/var/lib/postgresql/data -…
Result type is an specialization is used in Rust for carrying computations that can fail. It’s a sum type/enum type that has two variants Ok and Err . It’s an alternative for exceptions that don’t change the natural calling/return control flow. Here is the class # nullable enable using System ; public abstract class Result < T , E > { Result () { } public sealed class Ok : Result < T , E > {…
Basically you use XCompose to change the keymap from ć to ç. Here is how: Create a .XCompose file in your home with this include "%L" <dead_acute> <c> : "ç" Also since I’m using gnome I needed this in my .xprofile export GTK_IM_MODULE=xim Thanks @FelipeOLTavares for helping me with this. Also archwiki has a page on .XCompose and pointed out the .xprofile need
FINALLY! Okay after a day struggling I could enable intelisense for F# files in vim using LanguageClient-neovim and Ionide-vim . It was not easy beacuse of the lack of the documentation. Install the plugins I’m using vim-plug , to install the required plugins I added this to my .vimrc Plug 'autozimu/LanguageClient-neovim', { \ 'branch': 'next', \ 'do': 'bash install.sh', \ } Plug…
ALE is a linting engine for vim, it works like a charm and I prefer it over Syntastic because it’s asynchronous which means it doesn’t block while you’re typing. Syntastic may have support for async now but I’m still on ALE. ALE has support for a lot of languages , the only exceptions that I faced were F# and Rust (Rust seems to work now), both can work with Syntastic but since I like ALE so much…
I have a problem with functions with the form F(a: STRING, b: STRING) where I swap a and b and only discover the problem latter on with a runtime error. I had this with ints too, where I was passing the id of the wrong table, and it was a mess to findout what was happening. When you’re programming with a dynamic typed language like Python and Ruby, having type errors at runtime is something that…
I’m working on a pretty new setup on Kubernets, we hadn’t setup CI yet so after updating an image I need tell Kubernets to take the new image This command proved to be usefull kubectl rollout restart deployment/my-deployment This will restart the deployment updating the image that is use. I hope we setup CI soon
layout: post title: Redirecting output to arbitrary commands in scripts tags: [shell,exec] — Suppose that you have a script that runs early in boot. There is no way to watch it because it runs before the SSH server starts, or ever if you have serial connection, its output is not captured by anybody. So you get stuck. Your script doesn’t work and you don’t know what to do because you don’t have any…
quilt make easy to create a series of patches for things that are not in git The usage is pretty simple, you do quilt new <patch_name> quilt add <some_file> # edit the file quilt refresh And it’s done. The patch can be found at patches/ folder. You can stack patchs with push and pop . It make really easy to create patches from configuration files.
I’ve been writing a lot of ansible playbooks recently. When programing on dynamic languages is pretty common to have into the text editor the ability to evaluate arbitrary code, being a whole file or a single line. Here is how to this with ansible! I wrote a simple vim plugin for enabling me to do so. It’s usage is very simple, follow on Installation If you’re not using vim-plug , I really…
You need first create a tunnel from a remote port to your 22 port. Then you use this port for doing the reversed sshfs mymachine $ > ssh root@remote -R 10000:localhost:22 remote # > remote # > remote # > sshfs -p 10000 myuser@localhost:/local/path /remote/mountpoint/path I use this to mount frontend projects on remote systems so that I can run webpack on my machine and have it deployed to a remote…
Just add the bellow to the script import code; code.interact(local=locals()) Cheers
I use vim on the terminal, but I face a problem from old ages. I never remember if I have a vim running or not. When I’m using vim and want to run a command I send it to foreground run the command and use fg to get back to vim. But the problem is that sometimes I forgot to use fg and end up with logs of vims running in background. Emacs has a server mode that deals with this kind of problem but…
I use to code by writting tests and fixing errors. When things get dirty, debug by printing make the whole code/fix flow really slow. In this situations I call for interative debuggers. I don’t really on fancy IDE stuff, usually there are magic lines that you paste in the code to get access to interactive debugging. With python you can do import pdb ; pdb . set_trace () Google for python pdb On…
Containers need to be small for building performance and to safe space. To do so they give on a lot of usefull tools that are valuable during troubleshooting. Because of this using troubleshooting network problems from inside containers can be a PIAS. Luckly there is a container image with network tools installed by default: docker run -ti amouat/network-utils bash Thanks amouat you helped a lot!…
From time to time I have to free some space on my Fedora machine. PackageKit seems to take a lot of space for caching, you can free it by sudo pkcon refresh force Regards
If you’re working with docker you may face out of space problems. You can free some space by removing the intermediate images that docker users to create the final images. This is the command docker rmi $(docker images -f 'dangling=true' -q) If you need free space this can be usefull too docker system prune Use it wisely Cheers
Long time since the last post. Let’s go straight to the point. Ofter we need to know or IP. I got a ISP that loves to change my IP ofentenly. After googling what is my ip for hundren of times I decided to take a better approach Well https://myip.com has an API that is really easy to consume. This oneliner help me lot: curl https://api.myip.com -s | perl -lane 'print $1 if /"ip":"(.*?)"/g' You can…
ipython shortcuts I just copied the shortcuts from the docs, so because the docs page is hidding the descriptions The orignial can be found here: https://ipython.readthedocs.io/en/6.5.0/config/shortcuts/index.html IPython shortcuts ¶ Available shortcut in IPython terminal. Warning This list is automatically generated, and may not hold all the available shortcut. In particular, it may depends on…
