Viewing profile — aweinstock

The post "A Very General Method of Computing Shortest Paths" ( https://r6.ca/blog/20110808T035622Z.html ) shows that the Gauss-Jordan algorithm for solving matrix equations, the Fl…

I do think adding a Noita-style cellular automaton would be fairly straightforward. Currently Veloren has water and lava, but neither will flow (e.g. if water blocks are manually p…

The contrast between Gauss-Jordan[0] and the Bareiss algorithm[1] is a good example of explicitly handling the length of the numbers in bits as part of the runtime. Gauss-Jordan is…

Section 5.13 advises building a custom type-and-mode checkers (per project, seemingly). Section 4.1 defines a specific type-and-mode system in enough detail that it seems machine-c…

LLVM calls the process of breaking a struct/object into dataflow variables "Scalar Replacement of Aggregates". https://llvm.org/doxygen/classllvm_1_1SROA.html#details

If your source language has some construct that you want to express as state machines (e.g. async, CPS, pattern match compilation), and you want to compile the state machine as dir…

It's definitely the case that some of the ELF header fields can be repurposed to store additional data, the following articles all address that optimization: http://www.muppetlabs.…

It's probably worth noting that the majority of the development on that library was done on April 1st 2019.

Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.

For a concrete example of how z3 differs from Coq, consider trying to prove that "for all integers x, there exists an integer y greater than x such that x divides y" (a subgoal of …

The Knight Capital incident lost $440m in 45 minutes to a mistake in software deployment: https://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stoc...

> not all assignment makes a function impure That's exactly what the ST monad/STRef's are for. {new,read,write}STRef let you manipulate mutable references while keeping track of th…

As an exercise in learning Coq, I've implemented a proof-carrying version of the partial-ordering relation: https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e95... There's …

For a concrete example of what exploitation of a JS engine bug looks like, PlaidCTF2016 had a challenge that allowed people to run JS in a patched version of V8 that deliberately i…

Rust's set types do implement the BitAnd and BitOr traits, which allow using the & operator for intersection, | for union (There's also a few others, like (Sub, -, set difference) …

Searching the history to enforce the threefold repetition rule[1] wouldn't be efficient, but the fifty-move rule[2] could be pretty cheaply implemented (one cell of state for a cou…

It's a monad in Rust too (with Some being return, and and_then[1] being >>=). Rust's generics just aren't yet[2] flexible enough to abstract over monads within the language. [1] ht…

Attacker-controlled format strings are very convenient bugs, but they can't do everything. Consider the program: int main() { char buf[20]; fgets(buf, sizeof buf, stdin); printf(bu…

Without this patch, using an information leak to bypass ASLR would be as simple as leaking any address in libc (__libc_start_main is often convenient since it's where main returns …

This is fairly readable (high-level) post on word embeddings: http://colah.github.io/posts/2014-07-NLP-RNNs-Representation...

Higher branching factor gets you a better constant factor because the depth of the tree is the base-(branching factor) logarithm of the number of nodes. The number of pointers you …

There's some more in-depth documentation in the repo in doc/user_guide.txt, at around line 520-ish. It has Common Lisp style defmacro (augmented with pattern matching), and Scheme-…