Prove Getting Started

Getting Started with Prove: Intent-First Programming

Prove is an intent-first programming language that compiles to C, then to native binaries. With a focus on clarity and safety, Prove makes you think about *what* your code should do before *how* it does it.

Why Prove?

Traditional languages let you write anything syntactically valid. Prove enforces intent through verbs that categorize what a function does:

• Pure verbs: transforms, validated, reads, creates, matches
• IO verbs: inputs, outputs
• Async verbs: detached, attached, listens

This makes code self-documenting and enables powerful tooling like the intent-driven completion system.

Your First Prove Program

Let’s write a simple program that reads numbers and returns their sum:

main()
from
    console("Enter numbers separated by spaces:")
    input as String = console()
    numbers as List = parse_numbers(input)
    total as Integer = sum(numbers)
    console("The sum is: {total}")

Breaking It Down

• main() – Every function is a verb declaring its intent. main is the only “special” case
• from block – Contains the implementation
• Variables – Declared with name as Type = value
• Expressions – No semicolons, no braces—just whitespace

Working with Types

Prove has strong, inferred types with refinement support. Constraints after `where` enforce runtime guarantees:

  type Percentage is Integer where 0 <= _ <= 100 
  type PositiveCount as Integer where > 0
  type ValidEmail as String where r"^[a-z]+@[a-z]+\.[a-z]+$"

## Pattern Matching

Instead of `if/else`, Prove uses match or the dedicated matches verb for branching:

matches classify(score Integer) String
from
    score < 60 => "F"
    score < 70 => "D"
    score < 80 => "C"
    score < 90 => "B"
    _ => "A"

Failable Functions

Functions that can fail return !:

inputs open_socket(port Integer) Integer!
from
    connection as Socket = socket("127.0.0.1", 9000)

Use ! to propagate errors:

inputs start_server(config_path String) Server!
from
    content = read_file(config_path)!
    config = parse_json(content)!
    server = create_server(config)!

Contracts and Proofs

Prove supports formal contracts for specifying preconditions and invariants:

transforms divide(a Integer, b Integer) Integer
  requires: b != 0
  ensures: result * b <= a && a < (result + 1) * b from a / b
from

prove build 
./dist/my_program 

Or check for errors without building:

prove check

What’s Next?

Explore the standard library for built-in functions
Read about the type system in depth
Try the examples directory Prove is still evolving—join the community and help shape the future of intent-first programming.

Questions or feedback? Open an issue on botwork or join the discussion in #prove channel on Libera IRC.

Please leave this field empty

Could we add you to our mailing list!

We don’t spam! Read our privacy policy for more info.

Check your inbox folder to confirm your subscription (lets pretend we never heard of spam for legit emails).