Skip to content

Instantly share code, notes, and snippets.


Block or report user

Report or block MaiaVictor

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
MaiaVictor / program.js
Last active Oct 14, 2019
Example interactive / effective program
View program.js
// The Program type is used to create an "interactive interface" between
// Formality and Moonad, allowing us to create Formality programs that interact
// with the user, access the internet, write to the disk or whatever else you
// want to allow the user to do
import Base@0
// Multiple effects:
// - Alerting a message
// - Prompting a yes/no question to the user

Introduction to dependent types


There is a full spectrum of type systems. You all know untyped languages. They look like this:

function get_at(idx, arr)


Who we are?

There is a full spectrum of type systems. In an untyped language, we can write some code like this:

function get_at(idx, arr) {
  return arr[idx];
View stuff.txt
In general, I think our short-term goal should be to make Provit a great place
for developing and using Formality apps. As we add features, Provit will slowly
become what we call Moonad.
- Give names and define the scope of each project and its desired features
(Provit, Forall, Monad, FPM, etc.)
- Documentation on Provit should be as good as ReadTheDocs. How do we
accomplish that? Multi-line comments? Markdown? Should we have a menu with
the file tree?
View gist:f20c96e2b83fd0c87cdd822aeb53307b
main :
{ P : Word -> Type
, X : P(0)
, Y : P(0)
, a : P(0) -> P(1)
, b : P(0) -> P(2)
, c : P(1) -> P(3)
, d : P(2) -> P(4)
, e : P(4) -> P(5)
, f : P(5) -> P(6)
View desubits_example.js
const lib = require("eth-lib");
// Ethereum address
var address = "0x742d35cc6634c0532925a3b844bc454e4438f44e";
// Converts to desubytes and back
var words = lib.desubits.fromBytes(address);
var bytes = lib.desubits.toBytes(words);
// Prints words
MaiaVictor /
Last active Sep 18, 2019
Task: inline fm-net's rewrite() function


The goal of this task is to:

  1. Fully inline rewrite() on either fm-net.js or fm-net.c, such that it ends up with only native operations, branching, arrays writes/read; basically turn it into an inline ASM.

  2. Remove middle-function array accesses. Instead, rewrite() must pre-load the 4 neighbor nodes of the active pair in local variables, work with them, and then rewrite that region when the function ends.

Those changes are not only to optimize rewrite() (we know the compiler already does a great job at inlining), but, mainly, to reveal optimizations that the compiler can't see, and to make it easier to port the code to the EVM.

// Specifies a bug-free vector-accessor function
Spec : Type
{len : Ind} -> // Given a length `len`
! { ~A : Type // And a type `A`
, idx : Fin(len) // And an index, `idx`, up to `len`
, vec : Vec(A, len) // And a vector, `vec`, with `len` elements of type `A`
// Returns the element `x` that is at index `idx` of that `vec`
} -> [x : A ~ At(A,x,len,idx,vec)]
MaiaVictor /
Created Sep 10, 2019
Example Formality (Data.List)
import Induction.Nat
import Relation.Equality
T List {A : Type}
| cons {head : A, tail : List(A)}
| nil
// ::::::::::::::::::::::
// :: Simple functions ::
// ::::::::::::::::::::::

The problem: theorem proving is so useful, but nobody uses it. Why?

  • Criticise other proof langs accessibility

    • Agda: unicode, agda-modes, EMACs lockdown

    • Coq: 3 different languages, too mathematical

  • Criticise other proof langs efficiency

You can’t perform that action at this time.