thealmarty

#include <iostream>
#include <vector>

void insertion_sort(std::vector<int> & v) {
  // invariant: the first i elements of v are sorted
  for(size_t i = 1; i < v.size(); ++i) {
    int value = v[i];
    size_t j = i-1;
    // invariant: elements of v from j+1 to i inclusive are sorted and >= value
    for(; j >= 0 && v[j] > value; --j) {

thealmarty

#include <stdio.h>

void insertion(int v[], int size) {
  // invariant: the elements of v before index i are sorted
  for(int i = 1; i < size; ++i) {
    int value = v[i];
    int j = i;
    // invariant: the elements of v between j and i are sorted and > value
    for(;j > 0 && v[j-1] > value; --j) {
      v[j] = v[j-1];

thealmarty

onePlusOne : 1+1=2
onePlusOne = Refl

thealmarty

MVP unification implementation plan

The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.

Stage 1: Type checker enhancement

At the time of writing, the first stage of the totality checker MVP is finished. But the second and third stages, namely type checking data type and function declarations are required before unification can be implemented.

At the end of this stage, conversion/type checking for constructors is implemented.

thealmarty

Efficient compilation of function definitions with pattern-matching

Function definitions with pattern-matching can be compiled into case-expressions for more efficient evaluation using the pattern matching compiler algorithm. The algorithm translates function definitions into case-expressions and avoids repeated examination of patterns.

I summarize the pattern matching compiler algorithm here as in chapter 5 of The implementation of functional programming languages.

The algorithm

A function definition of the form

thealmarty

Unification in Idris 2

Unification concerns type/conversion checking with the presence of meta-variables. Meta-variables are variables with unknown values but type checking/elaboration progress could generate constraints that these variables have to satisfy and thus find the solutions to these variables. Implicits (and implicit arguments) are inferred by unification.

Conversion checking (of terms and closures) determines whether the two inputs are equivalent. Similarly, unification determines whether the two inputs are equivalent with the presence of meta-variables. Naturally, unification is implemented as an extension to conversion checking.

thealmarty

Lessons from Idris 2

This note summarizes what Juvix can learn from the implementation of Idris 2. References:

• The paper.
• Scottish summer school 2020 slides/notes.
• Video lectures of the summer school.
• The implementation documentation.

Syntax/theory on linearity

thealmarty

Potential Juvix features enabled by graph neural networks and machine learning

The rapid development of machine learning (ML) enables practical applications including in smart contract development. As a superior smart contract language, Juvix can provide extra support using ML in the following fronts:

1. Generate correctness proofs

See this paper. When combining the mechanics of Proverbot9001, CoqHammer and CoqGym, a meaningful portion (28%) of the correctness proofs of CompCert (written in Coq) was generated. Note that the difficulties of the generated proofs are evenly distributed - i.e., it is not only generating proofs that are trivial for users to write.

Juvix is built with the intent that smart contracts written in it are more secure because users can write proofs to prove important properties of a contract. However, writing proofs is a tedious and costly task. Juvix would be much more attractive if it can write a significant portion of the proof

thealmarty

type account = {
  balance : nat;
  allowances : (address, nat) map;
}

type storage = {
  accounts : (address, account) big_map;
  version : nat; 
  totalSupply : nat;
  name : string;

thealmarty

--Factorial function, short/standard version.
  
fact 0 = 1
fact n = n * fact (n - 1)

main = do
  print (fact 5)