Programming general

A collection of 4 posts

4 min read

Tail call functions on Rust I

MotivationRecursive functions are often a great way of writing declarative programs. This allows for greater expressiveness on the making process. However, they come with a catch: slowness and stack overflow, which is not great. The so-called tail call functions have a specific form that can be transform into normal jump

Read more
2 min read

Proving things with Kind

Kind is a dependently typed programming language made by uwu-tech that I recently discovered through GitHub. Unlike Agda, Coq and co., Kind doesn't rely on a ML-esque syntax, but rather in one that resembles Typescript or Rust, which is interesting. It also has a small core and two main implementations;

Read more
5 min read

Agda Fundamentals: (I / 1)

The following article is part of some meetings discussing Dependent Types between people in my college. I hope it can also be useful to someone else. Either way, this is just the «article» version of a couple of md slides that I made for it.

Read more