Max Taylor

Max Taylor

Formal Methods Scientist @ INL

Posts by Tags

ai

c++

A Concept and Template Meta-programming Approach to Session Types in C++

16 minute read

Published:

Introduction

Programs communicate – whether with other programs or humans. Software developers write programs with a protocol in mind. Sometimes there’s documentation for the protocol. But there’s no mechanism that keeps implementation and documentation in sync. Bugs occur when protocols diverge.

fstar

Using F* to Formally Verify Programs

30 minute read

Published:

Formal methods are currently not widely embraced due to their perceived difficulty. However, the landscape is changing with the emergence of new technologies that make formal methods more accessible than ever before. F*, developed by Microsoft Research, is a groundbreaking functional language that combines dependent types and proof-oriented features. By bridging the gap between programming and proving, F* facilitates a gradual adoption of formal methods by software engineers. In this post, I will provide an introduction to the basics of F* and demonstrate how we can leverage its capabilities to verify a solution to a LeetCode problem. I can’t cover all the background material needed to understand F* in this post. I assume that you have some experience in a language like Haskell or OCaml.

gpt

lisp

programming puzzles

Using F* to Formally Verify Programs

30 minute read

Published:

Formal methods are currently not widely embraced due to their perceived difficulty. However, the landscape is changing with the emergence of new technologies that make formal methods more accessible than ever before. F*, developed by Microsoft Research, is a groundbreaking functional language that combines dependent types and proof-oriented features. By bridging the gap between programming and proving, F* facilitates a gradual adoption of formal methods by software engineers. In this post, I will provide an introduction to the basics of F* and demonstrate how we can leverage its capabilities to verify a solution to a LeetCode problem. I can’t cover all the background material needed to understand F* in this post. I assume that you have some experience in a language like Haskell or OCaml.

python

rust

Rust: Generics Considered Colorful

4 minute read

Published:

This post shows that Rust’s generics are colorful. I’ll demonstrate an example to show what I mean, and what the problems are.

session types

A Concept and Template Meta-programming Approach to Session Types in C++

16 minute read

Published:

Introduction

Programs communicate – whether with other programs or humans. Software developers write programs with a protocol in mind. Sometimes there’s documentation for the protocol. But there’s no mechanism that keeps implementation and documentation in sync. Bugs occur when protocols diverge.

template metaprogramming

A Concept and Template Meta-programming Approach to Session Types in C++

16 minute read

Published:

Introduction

Programs communicate – whether with other programs or humans. Software developers write programs with a protocol in mind. Sometimes there’s documentation for the protocol. But there’s no mechanism that keeps implementation and documentation in sync. Bugs occur when protocols diverge.

types

Rust: Generics Considered Colorful

4 minute read

Published:

This post shows that Rust’s generics are colorful. I’ll demonstrate an example to show what I mean, and what the problems are.

A Concept and Template Meta-programming Approach to Session Types in C++

16 minute read

Published:

Introduction

Programs communicate – whether with other programs or humans. Software developers write programs with a protocol in mind. Sometimes there’s documentation for the protocol. But there’s no mechanism that keeps implementation and documentation in sync. Bugs occur when protocols diverge.