• Formal System

    A formal system consists of axioms (statements that are true) and rules (how axioms can be manipulated). New axioms can be deduced from other axioms and rules. You formalize a system when you start defining these statements and rules.

    A formal system is consistent when you can’t simultaneously prove and disprove an axiom. An inconsistent system would not be very useful e.g. a weather forecasting system that predicts it will rain and not rain at the same time.

    A formal system is a complete system when all statements in the system can be proved or disproved thereby allowing you to know everything about the system.

    See also:

  • EBNF

    A context-free grammar can be described using Extended Backusโ€“Naur form (EBNF) notation. This higher ‘metasyntax’ describes how another grammar should be parsed. This makes it a useful portable format for multiple programming languages to parse the same thing (if your system can read EBNF grammars it can parse a multitude of other grammars).

    For example, this EBNF loosely defines org-mode syntax:

    <DOC> = preamble heading*
preamble = [title] [author]
title = <'#+title'> text EOL
author = <'#+author'> text EOL
heading = level heading-text content*
<EOL> = '\n' | '\r' | #'$'
<SPC> = ' '
level = #'\*{1,}' SPC
heading-text = [status SPC] !status #'^.+'
text = #'^.+'
<content> = (EOL (EOL | heading | !level text))
todo = 'TODO'
done = 'DONE'
status = todo | done

    See also:

  • Modelica

    A modeling programming language and environment that provides a way to express, simulate, and optimize systems (usually physical).

    Most of the time, writing an algorithm is to write a specific solution to a certain problem. When doing mathematical modeling, we are collecting data from a simulation of equations that describe the problem.

    See also:

  • Gรถdel's Incompleteness Theorem

    A formal system (one that is consistent never yields a false statement) can not also be a complete system (containing all true statements)–there will always be statements that are unprovable yet true (i.e. G-statement).

    The proof is derived from Principia Mathematica (PM) logic looking at number theory. You can build new theorems from axioms that are true infinitely but, because it is infinite, it can not contain every true statement.

    That means there is always some truths that can’t be captured by a single system no matter how elaborate or seemingly robust. That’s why it’s important to have multiple systems and acknowledge you will always be limited in understanding the fullness of anything described by a formal system.

    See also:

  • Graphviz

    A declarative language for describing diagrams and an environment that renders .dot files into images. Since the diagram is written in code, it can be checked into version control and updated later which is much easier than a team need to use a separate (usually commercial program) to share a file to make updates.

  • Visitor Pattern

    A pattern for traversing a tree of heterogeneous objects. Decoupling the algorithm for traversing the tree and the code operating on the objects leads to a much cleaner (and easily extensible) code.

    Example usages include traversing an AST, the AST does not need to be changed to accomodate new code that is operating on it e.g. linters.

  • COVID-19

    A corona virus that became a global pandemic. The number of cases has surpassed 2MM and over 500 thousand people have died (at time of writing).

    Besides a health crisis, COVID-19 also created an economic crisis as countries shut down and placed restrictions on gatherings of people and whether businesses could operate.

  • Silurian Hypothesis

    Posits that there were previous civilizations on Earth before humans. Some scientists are conducting research to see if we could detect changes in things like atmospheric carbon, plastics, and nuclear fallout since it’s highly likely no other physical evidence would exist e.g. buildings and artifacts.

  • Literate Programming

    Intertwines documentation and source code which emphasizes the need for code to not only be understood by the compiler, but also by future engineers trying to reason about your code.

    Introduced by Donald Knuth in his book Literate Programming written in 1984 and implemented in the CWEB tool.

    Literate programming with org-mode

    Here’s an example of weaving the execution of code into this document which exports both the code block and output:

    import random
print random.randrange(0, 100)

    54

    To tangle this code such that it exports to a source code file we can add the following heading to the source block tangle: hello_world :exports none which will export the code block to a file hello_world.py.

    Read more about literate programming in org-mode using org-babel

  • R Value

    A rating for the ability of a virus to spread. R of 1 would indicate each infected person infects one person. Anything higher than 1 has the potential to grow the number of cases exponentially (i.e. an outbreak or pandemic). For example, measles had an R value of 15.

    This is similar to big O notation in estimating computation complexity. R1 would be constant time and R1+ would be O(N^1+).

  • SPAC IPO

    A shell holding company goes public with the intention of raising money to merge with a private companyโ€”effectively making the private company public without having to go through the listing process.

    While the fees tend to be higher than the private company going through the process of IPO-ing, they only need to make a deal with a single party (the SPAC) which significantly simplifies the process.

    See also:

  • Planck's Principle

    Scientific change doesn’t happen because because people change their mind, but because the next generation of scientists have different views.

    This is similar to startups and larger companies. As new people come in, they bring in new ideas and change happens (both good and bad).