Herbie uses the FPCore format to specify an input program, and has extensive options for precisely describing its context.

The Herbie web shell takes input in a subset of the math.js syntax. The web shell automatically checks for syntax errors, and provides a graphical user interface for specifying the input domain. The web shell converts the mathematical expression and input ranges into FPCore before sending it to Herbie.

Herbie's command-line and batch-mode tools use FPCore format to describe mathematical expressions. FPCore looks like this:

(FPCore (inputs ...)properties ...expression)

(FPCorename(inputs ...)properties ...expression)

Each `input` is a variable name, like `x`

,
used in the `expression`. Properties are used to specify
additional information about the `expression`'s context.
If `name` is specified, the function can be referenced in
subsequent FPCore declarations in the file.

The expression is written in prefix form, with every function call
parenthesized, as in Lisp. For example, the formula for the
hypotenuse of a triangle with legs *a* and *b* is:

(FPCore (a b) (sqrt (+ (* a a) (* b b))))

The semicolon (`;`) character introduces a line comment.
We recommend the `.fpcore`

file extension for Herbie input files.

Herbie supports all functions from math.h with floating-point-only inputs and outputs. The best supported functions include:

`+`

,`-`

,`*`

,`/`

,`fabs`

- The usual arithmetic functions
`sqrt`

,`cbrt`

- Square and cube roots
`pow`

,`exp`

,`log`

- Various exponentiations and logarithms
`sin`

,`cos`

,`tan`

- The trigonometric functions
`asin`

,`acos`

,`atan`

,`atan2`

- The inverse trigonometric functions
`sinh`

,`cosh`

,`tanh`

- The hyperbolic functions
`asinh`

,`acosh`

,`atanh`

- The inverse hyperbolic functions
`fma`

,`expm1`

,`log1p`

,`hypot`

- Specialized numeric functions

Herbie also supports the constants `PI`

and `E`

. Use `-`

for both subtraction and negation.

Herbie links against your computer's `libm`

to
evaluate these functions. So, each function has the same behavior in
Herbie as in your code. You can instead use
the `racket`

precision if you
instead want reproducible behavior.

FPCore uses `if`

for conditional expressions:

(ifcondif-trueif-false)

The conditional

may use:
`cond`

`==`

,`!=`

,`<`

,`>`

,`<=`

,`>=`

- The usual comparison operators
`and`

,`or`

,`not`

- The usual logical operators
`TRUE`

,`FALSE`

- The two boolean values

The comparison functions support chained comparisons with more than two arguments.

Intermediate variables can be defined
using `let`

and `let*`

:

(let ([variablevalue]...)body)

(let* ([variablevalue]...)body)

In both `let`

and `let*`

,
each `variable` is bound to its `value` and can be
used in the `body`. The difference between `let`

and `let*`

is what order the values are
evaluated in:

`let`

expressions- In a
`let`

expression, all the values are evaluated in parallel, before they are bound to their variables. This means that later values can't refer to earlier variables in the same`let`

block. `let*`

expressions- A
`let*`

block looks the same as a`let`

block, except the values are evaluated one at a time, and later values can refer to earlier variables.

Unless you have a lot of Lisp experience, you'll probably
find `let*`

more intuitive.

Internally, Herbie treats intermediate values only as a notational convenience, and inlines their values before improving the formula's accuracy. Using intermediate variables will therefore not produce a more accurate result or help Herbie run faster.

In some cases, your input program is an approximation of some
more complex mathematical expression. The `:spec`

(for
“specification”) lets you specify the more complex ideal case.
Herbie will then try to modify the input program to make it more
accurately evaluate the specification.

For example, suppose you want to evaluate `sin(1/x)`

via a series expansion. Write:

(FPCore (x) :spec (sin (/ 1 x)) (+ (/ 1 x) (/ 1 (* 6 (pow x 3)))))

Herbie will only use the `:spec`

expression to
evaluate error, not to search for accurate expressions.

By default, the arguments to formulas are assumed to be
arbitrarily large or small floating-point numbers. However, in most
programs a smaller range of argument values is possible.
The `:pre`

property (for “precondition”) describes this
smaller range.

Preconditions use comparison and boolean operators, just like conditional statements:

(FPCore (x) :pre (< 1 x 10) (/ 1 (- x 1)))

Herbie is particularly efficient when when the precondition is
an `and`

of ranges for each variable, but more complex
preconditions also work.

Herbie supports both single- and double-precision values; you can
specify the precision with the `:precision`

property:

`binary32`

- Single-precision IEEE-754 floating point
`binary64`

- Double-precision IEEE-754 floating point
`racket`

- Like
`binary64`

, but using Racket math functions rather than your computer's`libm`

.

By default, `binary64`

is assumed. Herbie also has
a plugin system to load additional
precisions.

Herbie won't produce mixed-precision code unless you allow it to
do so, using the `:herbie-conversions`

property:

`:herbie-conversions`

([`prec1``prec2`] ...)- Expressions in precision
`prec1`

, can be rewriten to use precision`prec2`

, and vice versa.

All conversions are assumed to be bidirectional. For example, if
you specify `:herbie-conversions ([binary64 binary32])`

,
Herbie will be able to add conversions between single- and
double-precision floating-point.

Herbie uses the `:name`

property to name FPCores in
its UI. Its value ought to be a string.

Herbie allows `:alt`

properties to specify additional
"developer targets"; these might be other alternatives you've tried
that you want to compare against.

Herbie's output provides additional information in custom properties:

`:herbie-status`

`status``status`describes whether Herbie worked: it is one of`success`

,`timeout`

,`error`

, or`crash`

.`:herbie-time`

`ms`- The time, in milliseconds, used by Herbie to find a more accurate formula.
`:herbie-error-input`

([`pts``err`] ...)- The average
`err`or of the input program at`pts`points. Multiple entries correspond to Herbie's training and test sets. `:herbie-error-output`

([`pts``err`] ...)- The computed average error of the output program, similar to
`:herbie-error-input`

.

Herbie's benchmark suite also uses properties for continuous integration, but these are not officially supported and their use is discouraged.