Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
71 lines (47 sloc) 2.68 KB

Hello, World!

Running a program

This is the "Hello, World!" in Formality:

import Base@0

main : Output
  print("Hello, world!")

Save this as hello.fm and run it with fm hello/main. This will use the interpreter to evaluate main and print its result. If everything works, you should see "Hello, world!" in your terminal.

Formality is a pure functional language: it has no global state or built-in IO. Instead, it just evaluates expressions, stringifies and outputs the result. As such, Output : Type and print : {str : String} -> Output are really just base-library (included on the first line) utilities that tell the CLI to pretty-print a string. main doesn't need to be an Output, though. It can be anything. For example, run this instead:

import Base@0

main : String
  "Hello, world!"

And it will output:

{cons, nil} => cons(1819043144,
{cons, nil} => cons(1998597231,
{cons, nil} => cons(1684828783,
{cons, nil} => nil)))

Which is how the string is encoded internally (a "Scott List" of 32-bit words storing an UTF-8 buffer).

Type-checking

Formality is also a proof language, which means it includes a powerful type-checker. You can call it with fm -t <file>/<term>. If your program is well-typed, you'll see its type. Otherwise, you'll see an error message explaining what is wrong. For example, given the program below:

import Base@0

main : String
  42

If you save it as wrong.fm and check with fm -t wrong/main, you'll see:

[ERROR]
Type mismatch.
- Found type... Num
- Instead of... String
- When checking 42

Because 42 isn't a String. It is recommended to always check a program's type before running it. Ill-typed programs aren't guaranteed to run correctly. Formality won't stop you from trying, though. In fact, type annotations are optional:

import Base@0

main
  "Hello, world!"

Note, though, that types are what allows Formality to verify mathematical proofs. That's because its type-system is so precise that you can specify complete algorithms with its type language. If your programs don't have types, then they can't be used in proofs at all. This will be explaned in later sections.

Optimal reductions

One of the most interesting aspects of Formality is that its programs can be evaluated optimally, as explained on this post, using an efficent graph-reduction system based on interaction combinators. To run your program using the optimal reduction algorithm, use the -o flag. To check other flags, just type fm on the terminal.

You can’t perform that action at this time.