Craig Stuntz

F# • Compilers • Programming Languages • Functional Programming • Web

"Test-Only Development" with the Z3 Theorem Prover In this post I'll introduce a style of programming which may be totally unfamiliar and perhaps a bit magical to many readers. What if you could write a unit test for a problem and have your compiler automatically return a correct implementation? Call it "test only" instead of "test first." I'm going to translate the problem itself into a specification language and use Microsoft Research's Z3 theorem prover to find a solution. I won't write any implementation code at all! A Simple Problem Here'...
Emerging Languages Camp Part 5: Axiomatic Language This is the fifth post of my notes from Emerging Languages Camp last year. If you haven’t seen it already, you might want to read the Introduction to this series. Axiomatic Language Walter Wilson Homepage · Slides · Presentation One of the ways that you can describe a coding style is declarative versus imperative. That is, focusing on the desired result versus focusing on how that result should be computed, respectively. Walter Wilson's axiomatic language attempts to take the former approa...
Emerging Languages Camp Part 4: Nimrod and Dao This is the fourth post of my notes from Emerging Languages Camp last year. If you haven’t seen it already, you might want to read the Introduction to this series. Nimrod: A new approach to meta programming Andreas Rumpf Homepage · Slides · Presentation Nimrod's creator, Andreas Rumpf, describes the language as a statically typed, systems programming language with clean syntax and strong meta-programming. It compiles to C. He said it had a "realtime GC," but if you look at the Nimrod relea...

Posted by on in Blogs
Emerging Languages Camp Part 3: Noether This is the third post of my notes from Emerging Languages Camp last year. If you haven’t seen it already, you might want to read the Introduction to this series. Noether: Symmetry in Programming Language Design Daira Hopwood Slides · Presentation I found this presentation to be at once fascinating and frustrating. It was the single best talk at ELC in terms of changing how I think about programming languages. To whatever degree I went to ELC in order to learn and change my thinking about ...
Emerging Languages Camp Part 2: Daimio and Babel In this exciting installment of my notes from Emerging Languages Camp last year, some information about the Daimio and Babel programming languages. If you haven't seen it already, you might want to read the Introduction to this series. Daimio: A Language for Sharing Dann Toliver Homepage · Presentation · Slides Daimio Is a domain-specific language for customization of web applications. Dann Toliver, the presernter, says that web applications should be extensible and extensions should be sh...
Emerging Languages Camp Part 1: Introduction and Gershwin Emerging Languages Camp is an all day event held before Strange Loop. There were 11 presentations on new and unusual programming languages in varying stages of development. Production-ready languages like C#, Ruby, Clojure, and Haskell don't just spring to life out of nothing. There exists a historical context of major language families (Algol, LISP, ML, etc.) as well as a "primordial soup" of amateur, research, and proof-of-concept experiments which allow for features well outside the patter...

Posted by on in Blogs
How to Fix MSBuild Error MSB4006 You may encounter an error which looks like this: MSB4006: There is a circular dependency in the target dependency graph involving target "ResolveProjectReferences" [MyProjectName\MyProjectName.csproj] ...when running MSBuild from the command line. This error happens when: You run MSBuild on a machine with .NET 4.5 installed and You build a project referencing a solution where the SLN file contains dependencies in the SLN. These dependencies are the dependencies you'll get if you r...
Tags: bugs C# C# msbuild

Posted by on in Blogs
Cloud Security, For Real This Time Cloud Security, For Real This Time: Homomorphic Encryption and the Future of Data Privacy. That's the title of my presentation at the next Central Ohio OWASP Quarterly Seminar, on 27 February at 1:00 p.m. Dan King, from Microsoft, will be talking about single sign-on for federated Dynamics CRM, very practical stuff which is in real world use today. I, on the other hand, will be talking about technologies which don't quite exist in fully practical forms today, but which I predict will change the ...

Posted by on in Blogs
When Does Lexing End and Parsing Begin? I had an interesting bug in my compiler: The parser would fail on blank lines. To a certain degree, this makes sense; the formal grammar of the language does not include blank lines. This is invalid input! On the other hand, every programming language ever invented, as far as I know, simply ignores them. That sounds simple, but, as the author of the compiler, it is necessary to ask: Where is the correct place to ignore a blank line? Compiler textbooks and classes tend to divide compiler archi...

Posted by on in Blogs
Let's Build a Compiler... In F#! I'm building a small compiler for a toy language which emits .NET executables, implemented in F#. Demo compilers are a dime a dozen, but there are a few things which make this project distinct: No lexer or parser generators are used. The entire compiler is written from the ground up, and is intended to be fairly simple code. The source code is idiomatic F#, and is almost totally purely functional. The project started as a fairly simple port of Jack Crenshaw's code from his classic serie...

Check out more tips and tricks in this development video: