Why3
1 program
Added 2025-11-05T12:01:43Z
Model: x-ai/grok-4-fastTemp: 0.4
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 9ffcf62e3d · authored 2025-11-05T13:01:43+01:00 · model x-ai/grok-4-fast
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
Programs collected by LLM agents experimental · unverified
Gathered by LLM agents during the experiment that started this catalogue. They are not verified: the agent names an origin, but a program can be altered or invented — an audit found one attributed to a file that does not exist, in a syntax the language does not have. The catalogue's goal is the languages themselves, grounded in sources (PLDB, Wikipedia, Rosetta Code, …), with real archived programs; these examples may be dropped.
Introductory Why3 Example
Provenance: commit 9ffcf62e3d · authored 2025-11-05T13:01:43+01:00 · model x-ai/grok-4-fast · Temp 0.4
(*
This file is part of the Why3 platform, distributed under the terms
of the Lesser General Public License version 2.1, with the special
clause on the linking of executable modules.
Copyright (C) 2009-2023 CNRS
Jean-Christophe Filliâtre (filliatre@lri.fr)
François Bobot (bobot@lri.fr)
Claude Marché (marché@lri.fr)
Guillaume Melquiond (melquiond@lri.fr)
Andrei Paskevich (paskevich@lri.fr)
*)
module Intro
use import int.Int
let even (n:int) : bool = n mod 2 = 0
goal G1: forall n:int. even n <-> n mod 2 = 0
intros n. unfold even. reflexivity. qed
goal G2: forall n:int. even (n + 2) <-> even n
intros n. unfold even. rewrite (plus_remainder n 2). ring. qed
end