1<!doctype html> 2<html lang="en"> 3 <head> 4 <link 5 rel="icon" 6 href="data:image/svg+xml,<svg xmlns=%22http://www.w3.org/2000/svg%22 viewBox=%220 0 100 100%22><text y=%22.9em%22 font-size=%2290%22>â</text></svg>" 7 /> 8 <meta charset="utf-8" /> 9 <meta content="width=device-width, initial-scale=1.0" name="viewport" /> 10 <title>Starling | Proof Assistant for Mathematicians</title> 11 <meta 12 name="description" 13 content="Starling is a proof assistant designed for ease of use." 14 /> 15
15<script src="https://cdn.tailwindcss.com?plugins=forms,container-queries"></script>
15 16 <link 17 href="https://fonts.googleapis.com/css2?family=Newsreader:ital,opsz,wght@0,6..72,200..800;1,6..72,200..800&family=Plus+Jakarta+Sans:ital,wght@0,200..800;1,200..800&display=swap" 18 rel="stylesheet" 19 /> 20 <link 21 href="https://fonts.googleapis.com/css2?family=Material+Symbols+Outlined:wght,[email protected],0..1&display=swap" 22 rel="stylesheet" 23 /> 24
24<script id="tailwind-config"> 25 tailwind.config = { 26 darkMode: "class", 27 theme: { 28 extend: { 29 colors: { 30 "tertiary-fixed": "#e2dfff", 31 "secondary-fixed": "#c3ecd0", 32 "error-container": "#ffdad6", 33 secondary: "#416650", 34 "outline-variant": "#c1c8c2", 35 "on-primary-fixed": "#002114", 36 "surface-container-highest": "#e4e2dd", 37 "on-primary": "#ffffff", 38 "primary-container": "#1b4332", 39 primary: "#012d1d", 40 "surface-dim": "#dbdad5", 41 "primary-fixed": "#c1ecd4", 42 "tertiary-container": "#2607c2", 43 "surface-container-lowest": "#ffffff", 44 "on-tertiary-container": "#9e9cff", 45 outline: "#717973", 46 "inverse-primary": "#a5d0b9", 47 "on-error": "#ffffff", 48 "on-secondary-fixed": "#002111", 49 "surface-variant": "#e4e2dd", 50 "on-tertiary-fixed": "#0f0069", 51 "secondary-container": "#c0e9ce", 52 "tertiary-fixed-dim": "#c3c0ff", 53 "on-tertiary": "#ffffff", 54 surface: "#fbf9f4", 55 "on-secondary-container": "#456a54", 56 "on-secondary": "#ffffff", 57 "on-surface": "#1b1c19", 58 "on-error-container": "#93000a", 59 "surface-bright": "#fbf9f4", 60 "on-secondary-fixed-variant": "#2a4e3a", 61 "surface-container-high": "#eae8e3", 62 "inverse-surface": "#30312e", 63 "secondary-fixed-dim": "#a7d0b5", 64 "on-tertiary-fixed-variant": "#3323cc", 65 "on-background": "#1b1c19", 66 "on-primary-container": "#86af99", 67 "surface-tint": "#3f6653", 68 "surface-container-low": "#f5f3ee", 69 "surface-container": "#f0eee9", 70 error: "#ba1a1a", 71 "inverse-on-surface": "#f2f1ec", 72 tertiary: "#160088", 73 background: "#fbf9f4", 74 "on-surface-variant": "#414844", 75 "on-primary-fixed-variant": "#274e3d", 76 "primary-fixed-dim": "#a5d0b9", 77 }, 78 borderRadius: { 79 DEFAULT: "1rem", 80 lg: "2rem", 81 xl: "3rem", 82 full: "9999px", 83 }, 84 fontFamily: { 85 headline: ["Newsreader", "serif"], 86 body: ["Plus Jakarta Sans", "sans-serif"], 87 label: ["Plus Jakarta Sans", "sans-serif"], 88 }, 89 }, 90 }, 91 }; 92 </script>
92 93 <style> 94 body { 95 font-family: "Plus Jakarta Sans", sans-serif; 96 } 97 .font-headline { 98 font-family: "Newsreader", serif; 99 } 100 101 .deep-shadow { 102 box-shadow: 103 0 1px 1px hsl(0deg 0% 0% / 0.011), 104 0 2px 2px hsl(0deg 0% 0% / 0.011), 105 0 5px 5px hsl(0deg 0% 0% / 0.011), 106 0 10px 10px hsl(0deg 0% 0% / 0.011), 107 0 18px 18px hsl(0deg 0% 0% / 0.011), 108 0 33px 33px hsl(0deg 0% 0% / 0.011); 109 } 110 111 .layered-card-shadow { 112 box-shadow: 113 0.3px 0.5px 0.7px hsl(var(--shadow-color) / 0.1), 114 0.8px 1.6px 2px -0.8px hsl(var(--shadow-color) / 0.1), 115 2.1px 4.1px 5.2px -1.7px hsl(var(--shadow-color) / 0.1), 116 5px 10px 12.6px -2.5px hsl(var(--shadow-color) / 0.1); 117 --shadow-color: 160deg 5% 20%; 118 } 119 120 .lush-shadow { 121 box-shadow: 122 0px 12px 24px -4px rgba(27, 28, 25, 0.04), 123 0px 24px 48px -8px rgba(27, 28, 25, 0.08); 124 } 125 126 .glass-nav { 127 backdrop-filter: blur(20px); 128 } 129 .murmuration-mask { 130 mask-image: radial-gradient( 131 circle at center, 132 black, 133 transparent 80% 134 ); 135 } 136 137 .reveal { 138 opacity: 0; 139 transform: translateY(30px); 140 transition: all 1.2s cubic-bezier(0.22, 1, 0.36, 1); 141 } 142 .reveal.active { 143 opacity: 1; 144 transform: translateY(0); 145 } 146 .reveal-delay-1 { 147 transition-delay: 0.1s; 148 } 149 .reveal-delay-2 { 150 transition-delay: 0.2s; 151 } 152 .reveal-delay-3 { 153 transition-delay: 0.3s; 154 } 155 </style> 156 </head> 157 <body 158 class="bg-surface text-on-surface selection:bg-tertiary-fixed selection:text-tertiary" 159 > 160 <nav 161 class="fixed top-0 w-full z-50 bg-[#fbf9f4]/80 dark:bg-[#1b1c19]/80 backdrop-blur-xl border-b border-outline-variant/10" 162 > 163 <div 164 class="flex justify-between items-center px-8 py-6 max-w-7xl mx-auto" 165 > 166 <a 167 class="text-2xl font-semibold italic text-[#012d1d] dark:text-[#fbf9f4] tracking-tight hover:scale-105 transition-transform duration-300" 168 href="/" 169 > 170 Starling 171 </a> 172 <div class="flex gap-12 items-center"> 173 <a 174 class="text-[#1b4332]/70 dark:text-[#fbf9f4]/70 font-medium hover:text-[#160088] transition-colors duration-300 text-sm tracking-wide" 175 href="docs/index.html" 176 >Documentation</a 177 > 178 <a 179 class="text-[#1b4332]/70 dark:text-[#fbf9f4]/70 font-medium hover:text-[#160088] transition-colors duration-300 text-sm tracking-wide" 180 href="editor/index.html" 181 >New</a 182 > 183 </div> 184 </div> 185 </nav> 186 <main class="relative overflow-hidden"> 187 <section 188 class="relative min-h-screen flex flex-col items-center justify-center pt-32 px-6 overflow-hidden" 189 > 190 <div 191 class="absolute inset-0 -z-10 opacity-20 murmuration-mask pointer-events-none" 192 > 193 <svg 194 fill="none" 195 height="100%" 196 viewbox="0 0 800 800" 197 width="100%" 198 xmlns="http://www.w3.org/2000/svg" 199 > 200 <circle 201 cx="200" 202 cy="300" 203 fill="#012d1d" 204 r="1.5" 205 ></circle> 206 <circle 207 cx="210" 208 cy="320" 209 fill="#012d1d" 210 r="1.5" 211 ></circle> 212 <circle cx="230" cy="315" fill="#160088" r="2"></circle> 213 <circle 214 cx="250" 215 cy="340" 216 fill="#012d1d" 217 r="1.5" 218 ></circle> 219 <circle cx="280" cy="330" fill="#012d1d" r="1"></circle> 220 <circle 221 cx="300" 222 cy="360" 223 fill="#160088" 224 r="2.5" 225 ></circle> 226 <circle 227 cx="400" 228 cy="400" 229 fill="#012d1d" 230 r="1.5" 231 ></circle> 232 <circle 233 cx="420" 234 cy="410" 235 fill="#012d1d" 236 r="1.5" 237 ></circle> 238 <path 239 d="M100 600 Q 250 450 400 600 T 700 600" 240 fill="none" 241 stroke="#c1c8c2" 242 stroke-width="0.5" 243 ></path> 244 </svg> 245 </div> 246 <div class="max-w-4xl text-center z-10 reveal">
247 <span 248 class="inline-block px-4 py-1.5 mb-8 text-xs font-bold uppercase tracking-[0.2em] text-on-surface-variant bg-surface-container-low rounded-full" 249 > 250 formal verification made accessible? 251 </span> 252 <h1 253 class="font-headline text-7xl md:text-8xl lg:text-9xl text-primary leading-[0.9] tracking-tight mb-12" 254 > 255 A proof assistant for the 256 <span class="italic">mathematician</span>. 257 </h1> 258 <div 259 class="flex flex-col md:flex-row items-center justify-center gap-8 mt-12 reveal reveal-delay-1" 260 > 261 <a 262 class="px-12 py-5 bg-gradient-to-br from-primary to-primary-container text-on-primary rounded-xl font-semibold text-lg hover:scale-[1.02] transition-transform duration-500 lush-shadow" 263 href="editor/index.html" 264 > 265 Start Formalizing 266 </a> 267 <p 268 class="text-on-surface-variant max-w-xs text-left text-sm leading-relaxed border-l border-outline-variant/30 pl-6" 269 > 270 Starling is an interactive theorem prover designed 271 for human intuition, not just programming expertise 272 or automation. 273 </p> 274 </div> 275 </div> 276 </section> 277 <section class="py-48 px-8 max-w-7xl mx-auto"> 278 <div class="grid lg:grid-cols-2 gap-24 items-center"> 279 <div class="relative group reveal"> 280 <div 281 class="absolute -inset-8 bg-secondary-container/10 rounded-[3rem] blur-3xl group-hover:bg-tertiary-fixed/20 transition-colors duration-1000" 282 ></div> 283 <div class="relative rounded-xl overflow-hidden"> 284 <img 285 alt="Starling code snippet" 286 class="w-full aspect-[4/5] object-cover" 287 src="assets/carbon.svg" 288 /> 289 </div> 290 </div> 291 <div class="space-y-10 reveal reveal-delay-1"> 292 <h2 293 class="font-headline text-5xl md:text-6xl text-primary leading-tight" 294 > 295 A Language for 296 <span 297 class="italic underline decoration-tertiary/20 underline-offset-8" 298 >Insight</span 299 > 300 </h2> 301 <p 302 class="text-xl text-on-surface-variant font-light leading-relaxed" 303 > 304 Starling enables mathematicians without a background 305 in functional programming to formalize mathematical 306 results. Built on top of Norman Megill's 307 <strong>Metamath</strong> and inspired by 308 <strong>Isabelle/Isar</strong>, the Starling 309 language offers readable syntax that is natural to 310 write or think in. 311 </p> 312 </div> 313 </div> 314 </section> 315 316 <section class="py-64 px-8 relative overflow-hidden"> 317 <div class="max-w-4xl mx-auto text-center reveal"> 318 <h2 319 class="font-headline text-6xl md:text-7xl text-primary mb-12" 320 > 321 Start your next proof. 322 </h2> 323 <div 324 class="flex flex-col md:flex-row justify-center items-center gap-8 reveal reveal-delay-1" 325 > 326 <a 327 class="px-12 py-5 bg-primary text-on-primary rounded-xl font-bold tracking-tight hover:scale-105 transition-all duration-300 lush-sha
327dow" 328 href="editor/index.html" 329 > 330 Launch Starling Editor 331 </a> 332 <a 333 class="px-12 py-5 text-primary font-bold border-b border-transparent hover:border-tertiary transition-all duration-300" 334 href="docs/index.html" 335 > 336 Explore Documentation 337 </a> 338 </div> 339 </div> 340 </section> 341 </main> 342 <footer 343 class="w-full bg-[#fbf9f4] dark:bg-[#1b1c19] border-t border-[#c1c8c2]/15" 344 > 345 <div 346 class="flex flex-col md:flex-row justify-between items-center px-12 py-16 w-full max-w-7xl mx-auto" 347 > 348 <div class="mb-8 md:mb-0 text-center md:text-left"> 349 <div 350 class="text-lg font-bold text-[#012d1d] dark:text-[#fbf9f4] mb-2 uppercase tracking-tighter" 351 > 352 Starling 353 </div> 354 <p 355 class="text-[#1b4332]/60 dark:text-[#fbf9f4]/60 text-xs tracking-widest uppercase" 356 > 357 © 2026 358 <a href="https://enderminyard.com">ENDER MINYARD</a> 359 </p> 360 </div> 361 <div class="flex flex-wrap justify-center gap-8 md:gap-12"> 362 <a 363 class="text-[#1b4332]/60 dark:text-[#fbf9f4]/60 text-xs uppercase tracking-widest hover:text-[#012d1d] dark:hover:text-[#ffffff] transition-all opacity-80 hover:opacity-100" 364 href="https://us.metamath.org/" 365 >metamath</a 366 > 367 <a 368 class="text-[#1b4332]/60 dark:text-[#fbf9f4]/60 text-xs uppercase tracking-widest hover:text-[#160088] dark:hover:text-[#ffffff] transition-all opacity-80 hover:opacity-100 font-semibold" 369 href="https://github.com/starlinglang/starling" 370 >github</a 371 > 372 </div> 373 </div> 374 <br /> 375 <br /> 376 <br /> 377 <br /> 378 </footer> 379 <div 380 class="fixed bottom-0 left-0 w-full h-24 bg-gradient-to-t from-surface to-transparent pointer-events-none z-40 backdrop-blur-[2px]" 381 ></div> 382
382<script> 383 const revealElements = document.querySelectorAll(".reveal"); 384 385 const revealObserver = new IntersectionObserver( 386 (entries) => { 387 entries.forEach((entry) => { 388 if (entry.isIntersecting) { 389 entry.target.classList.add("active"); 390 // Once visible, we can unobserve if we only want it to reveal once 391 // revealObserver.unobserve(entry.target); 392 } else { 393 // Optional: remove class to animate out when scrolling back up 394 entry.target.classList.remove("active"); 395 } 396 }); 397 }, 398 { 399 threshold: 0.15, 400 rootMargin: "0px 0px -50px 0px", 401 }, 402 ); 403 404 revealElements.forEach((el) => revealObserver.observe(el)); 405 </script>
405 406 </body> 407</html>
Line numbers count LF bytes from the start of the resource, as the search results do. Vendor segments are library code the classifier recognised; they are stored but not indexed. Bytes are shown as Latin1 characters, one per byte.