Don’t worry … it’s super easy 🙃
SMT is a form of logic programming that helps you reason about the design and behavior of systems. The reason why I was interested in writing a language in this space is because the existing languages assume you have a background in predicate logic and the mathematical notations and terminology that comes along with that. And so most software engineers can’t take advantage of the best tools because they do not understand what the tool does or how to use it.
It’s really an age old dilemma in computers: “real programmers” write code in C. No “real programmers” write code in Assembly. No “real programmers” write code in binary. No, wait, “real programmers” use butterflies. There is always tension between the people who think that those that want the power of technology should just put in the work to understand it and people who believe the tools should make that power accessible to as many people as possible.
I was interested in whether I could write a language that made it easier for people to construct formal models of computer systems.
And today I’m releasing some documentation on how to write models in Fault, and asking you guys to play around with it.
Two reasons really: First you will almost certainly break Fault’s compiler in strange and wonderful ways and I hope that when you do so you’ll open an issue here so that I can stabilize and further improve it.
Second, I’m genuinely curious how people think about systems and what kinds of models they will build.
I’m also sitting down with people and asking them to run through the installation of the compiler on their machines to get an idea of how well that works and whether there are any cross compatibility issues. If you’re up for that, book some time on my calendar.