Active sonar — the world's first FMCW radar

How does a bat see with sound?

An 80→30 kHz chirp, a round-trip echo, a matched filter — the same algebra every modern radar uses, 50 million years older.

emitted chirp · received signal with buried echo · matched-filter peak

1. Emitted chirp — 80 → 30 kHz over 3 ms

2. Received signal — echo from 3.0 m @ +2.0 m/s

3. Matched-filter output — pulse-compression peak

Detected distance

3.00 m

True distance

3.00 m

Error

-0.004 m

Target distance: 3.00 m

Radial velocity: +2.0 m/s (+ away, − approaching)

↑ Audible chirp uses your current distance + velocity. Slow, approaching prey sounds higher-pitched; far targets have a faint delayed echo.

Tap to drop obstacles. Ping to hear the bat’s sonar.

orange wave = outbound chirp · green wave = echo · click fires when round-trip arrives

The math behind it

Each function carries a @verify contract that compiles to a Lean theorem about its bounds. The same source compiles to C, Verilog, HLSL, and 28 more targets. View the experiment on GitHub →

chirp.emlchain 0

module chirp;

const F_START_HZ:  Real = 80000.0
const F_END_HZ:    Real = 30000.0
const DURATION_S:  Real =  0.003

@verify(lean, theorem = "chirp_frequency_in_band")
fn chirp_frequency(t_s: Real) -> Real
    requires (t_s >= 0.0 and t_s <= DURATION_S)
    ensures  (result >= F_END_HZ and result <= F_START_HZ)
{
    clamp(F_START_HZ + (F_END_HZ - F_START_HZ) * (t_s / DURATION_S),
          F_END_HZ, F_START_HZ)
}

echo_distance.emlchain 0

module echo_distance;

const SPEED_OF_SOUND_M_S: Real = 343.0

@verify(lean, theorem = "delay_to_distance_nonneg")
fn delay_to_distance(delay_s: Real) -> Real
    requires (delay_s >= 0.0)
    ensures  (result >= 0.0)
{
    SPEED_OF_SOUND_M_S * delay_s / 2.0
}

doppler.emlchain 0

module doppler;

const SPEED_OF_SOUND_M_S: Real = 343.0

@verify(lean, theorem = "doppler_velocity_bounded")
fn doppler_velocity(f_emit: Real, f_recv: Real) -> Real
    requires (f_emit > 0.0 and f_recv > 0.0)
    ensures  (result <=  SPEED_OF_SOUND_M_S)
    ensures  (result >= -SPEED_OF_SOUND_M_S)
{
    clamp(SPEED_OF_SOUND_M_S * (f_emit - f_recv) / f_emit,
          -SPEED_OF_SOUND_M_S, SPEED_OF_SOUND_M_S)
}

matched_filter.emlchain 0

module matched_filter;

@verify(lean, theorem = "matched_filter_cauchy_schwarz")
fn matched_filter_score(t_amp: Real, r_amp: Real, overlap: Real) -> Real
    requires (t_amp >= 0.0 and r_amp >= 0.0)
    requires (overlap >= -1.0 and overlap <= 1.0)
    ensures  (result <=   t_amp * r_amp)
    ensures  (result >= - t_amp * r_amp)
{
    t_amp * r_amp * overlap
}

Same EML pipeline. Different sense.

Eight more cross-species sensor models live alongside this one — bat sonar, owl 3D hearing, pit-viper infrared, dog olfaction, pigeon magnetoreception, shark electric sense, mantis shrimp 16-channel hyperspectral, spider web vibration.

See all nine senses →