The author shares sixteen compelling reasons to love programming languages, focusing on their human, mathematical, and community aspects that enrich the field.
About:
Daniel works at HPE on the Chapel language team, with interests in programming languages and compilers, and enjoys writing technical content.
Website:
Specializations:
Interests:
Incoming Links:
Outgoing Links:
Subscribe to RSS:
The text discusses Chapel's runtime types as an alternative to dependent types. It compares Chapel's array types to C++'s std::array and explains the benefits of knowing the size of a data structure. It also addresses the difficul...
The text discusses the implementation and verification of 'Static Program Analysis' in Agda, focusing on verifying the forward analysis. It covers the high-level algorithm, correctness properties of the semantic function, correctn...
The post discusses the implementation and verification of static program analysis in Agda, focusing on forward analysis. It covers the construction of a finite-height lattice to contain information about each variable at each node...
The blog post discusses the implementation and verification of 'Static Program Analysis' in Agda. It covers the formal semantics of the programming language, control flow graphs, and the connection between the two. The author expl...
The blog post discusses the implementation and verification of 'Static Program Analysis' in Agda, focusing on Control Flow Graphs (CFGs). It explains the basic definition of CFGs, combining graphs, additional functions, and connec...
The blog post discusses the implementation and verification of 'Static Program Analysis' in Agda, focusing on the syntax and semantics of a simple programming language. It explains the rules for evaluating expressions, simple stat...
The post discusses the fixed-point algorithm used in lattice-based static analyses, which iteratively combines facts from a program into new ones. The algorithm is guaranteed to terminate and provide a fixed point. The author also...
The blog post discusses the formalization of finite height lattices, specifically the 'above-below' lattice, the product lattice, and the map lattice. The author explains the formalization process and the Agda proofs of the proper...
The blog post discusses the implementation and verification of 'Static Program Analysis' in Agda, focusing on combining lattices. It covers the Cartesian Product Lattice, the Map Lattice, and the theory and implementation of these...
0Untitled Short Story
2024-08-02 •
The story describes the discovery of the Everpresent Void at a children's birthday party, and how it became a popular phenomenon among kids and adults. The Void was a black fluid that responded to the observer's mind and was used ...
The blog post discusses the implementation and verification of 'Static Program Analysis' in Agda, focusing on lattices and monotone frameworks. It explains the importance of specificity in program analysis and how lattices are use...
The blog post discusses the author's journey to formalize Static Program Analysis in Agda, covering topics such as lattices, combining lattices, the fixed-point algorithm, and correctness. The author also outlines the subsequent p...
0Microfeatures I Love in Blogs and Personal Websites
2024-06-23 •
The blog post discusses various microfeatures that can be added to personal websites and blogs to enhance the reading experience. These microfeatures include sidenotes, tables of contents, page progress indicators, easily linkable...
0Integrating Agda's HTML Output with Hugo
2024-05-30 •
The blog post discusses integrating Agda's HTML output with Hugo, allowing clickable HTML pages for Agda code. The author shares a script to transfer links from an Agda HTML file into Hugo's HTML output, making it possible to embe...
0The "Deeply Embedded Expression" Trick in Agda
2024-03-11 •
The blog post discusses a trick called 'Deeply Embedded Expressions' in Agda, which simplifies proofs in a large Agda project. The author explains the motivation behind developing the trick, the challenges faced in proving certain...
The blog post discusses the concept of inference rules in programming language theory, particularly in the field of programming languages. It introduces Bergamot, a new programming language that allows for the interactive explorat...
0My Favorite C++ Pattern: X Macros
2023-10-14 •
The blog post discusses the X Macros pattern and its applications in the Chapel compiler. It explains how the pattern is used to generate code for string interning, AST class hierarchy, and Python class hierarchy. The post also co...
0The "Is Something" Pattern in Agda
2023-09-01 •
The blog post discusses the 'IsSomething' pattern in Agda, a functional programming language with a Haskell-like syntax. The pattern involves parameterizing by operations and using parameterized modules to avoid repetitive argumen...
0Proving My Compiler Code Incorrect With Alloy
2023-06-05 •
The author describes his experience applying Alloy to a real part of the Chapel compiler. He explains the problem at hand, the scope resolution in Chapel, and the process of resolution. He also describes the process of modeling fl...
0Search as a Polynomial
2023-05-23 •
The blog post discusses the connection between polynomials and a general concept of search, exploring the space of possible routes. It explains how polynomials can be used to represent any combination of trips of various lengths a...
0Generalizing Folds in Haskell
2022-04-22 •
The blog post discusses the concept of generalizing folds in Haskell, focusing on recursive functions, recursive data types, and base functors. It explains how to transform recursive functions and data types, and how to define rec...
The blog post discusses the author's process of deploying multiple versions of his blog using NixOS and Flakes. The author explains the constraints he faced, the reasons for choosing Flakes, and the final result of his configurati...
0Digit Sum Patterns and Modular Arithmetic
2021-12-30 •
The blog post discusses digit sum patterns and modular arithmetic. It explains how to draw patterns from numbers and the mathematical reasoning behind it. The author also provides code to replicate the behavior and generalizes the...