Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code

/-- A prime is a number larger than 1 with no trivial divisors -/
def IsPrime (n : Nat) := 1 < n ∧ ∀ k, 1 < k → k < n → ¬ k ∣ n

-- 'Grind' efficiently manages complex pattern matching and
-- case analysis beyond standard tactics.
example (x : Nat) : 0 < match x with
  | 0   => 1
  | n+1 => x + n := by
  grind

-- Automatically solves systems of linear inequalities.
example (x y : Int) :
    27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45
    → -10 ≤ 7*x - 9*y → 7*x - 9*y > 4 := by
  grind

Does anyone have experience with Lean? Can it be useful for implementing algorithms or logic beyond mathematical proofs, for software libs?

Hare’s boringness is a feature, not a bug. Our goal is not to make programming exciting again, but to make it easy to write simple, obvious programs which are optimized for reliability and longevity. An exciting programming language cannot meet that goal as effectively as Hare does. We have instead sought out the smallest and simplest language design which accommodates these goals. Because we have relatively few features, Hare programs tend to converge upon the single obvious way of solving their problems with the tools at their disposal.

Examples from the README

[
  { "let": { "name": "JSON", "times": 3 } },
  {
    "for": {
      "var": "i",
      "from": 1,
      "to": "times",
      "do": [
        { "print": { "add": ["Hello ", "name"] } }
      ]
    }
  }
]

[
  { "import": "system.jpl" },
  { "print": { "call": { "now": [] } } },
  { "print": { "call": { "osName": [] } } },
  { "print": { "call": { "cpuCount": [] } } },
  { "let": { "a": 9, "b": 4, "name": "JPL" } },
  { "print": { "add": ["\"a + b = \"", { "add": ["a", "b"] }] } },
  { "print": { "mul": ["a", "b"] } },
  { "print": { "div": ["a", "b"] } },
  { "print": { "mod": ["a", "b"] } },
  { "print": { "&": [6, 3] } },
  { "print": { "||": [false, true] } },
  { "print": { "gt": ["a", "b"] } },
  { "def": { "sq": { "params": ["x"], "body": [{ "return": { "mul": ["x", "x"] } }] } } },
  { "print": { "call": { "sq": [5] } } },
  { "def": { "greet": { "params": ["who"], "body": [{ "return": { "add": ["\"Hi, \"", "who"] } }] } } },
  { "print": { "call": { "greet": ["\"JSON Fan\""] } } },
  { "if": { "cond": { "<": ["b", "a"] }, "then": { "print": "\"b < a 👍\"" }, "else": { "print": "\"b >= a 🤔\"" } } },
  { "for": { "var": "i", "from": 1, "to": 3, "step": 1, "do": [ { "print": { "call": { "sq": ["i"] } } } ] } },
  { "print": "\"All features in one! 🎉\"" }
]

[
// 🚀 Welcome to JPL — JSON Programming Language!

// Import system utilities for fun stuff
{ "import": "system.jpl" },

// Print system info
{ "print": { "call": { "now": [] } } },
{ "print": { "call": { "osName": [] } } },
{ "print": { "call": { "cpuCount": [] } } },

// Define a math function to square a number
{
  "def": {
    "square": {
      "params": ["x"],
      "body": [
        { "return": { "mul": ["x", "x"] } }
      ]
    }
  }
},

// Greet a user
{
  "def": {
    "greet": {
      "params": ["name"],
      "body": [
        { "return": { "add": ["Hello, ", "name"] } }
      ]
    }
  }
},

// Declare variables
{ "let": { "a": 7, "user": "Kapil" } },

// Use greet function and print
{ "print": { "call": { "greet": ["user"] } } },

// Conditional message
{
  "if": {
    "cond": { ">": ["a", 5] },
    "then": { "print": "a is greater than 5" },
    "else": { "print": "a is 5 or less" }
  }
},

// Loop with break and continue
{
  "for": {
    "var": "i",
    "from": 1,
    "to": 10,
    "step": 1,
    "do": [
      { "if": { "cond": { "eq": ["i", 3] }, "then": { "continue": true } } },
      { "if": { "cond": { "gt": ["i", 7] }, "then": { "break": true } } },
      { "print": { "call": { "square": ["i"] } } }
    ]
  }
},

// Fun ending message
{ "print": "🎉 Done with curly braces and JSON fun!" }
]

The population (especially the younger generation, who never seen a different kind of technology at all) is being conditioned by the tech industry to accept that software should behave like an unreliable, manipulative human rather than a precise, predictable machine. They're learning that you can't simply tell a computer "I'm not interested" and expect it to respect that choice. Instead, you must engage in a perpetual dance of "not now, please" - only to face the same prompts again and again.

Developer experience, concrete examples, contextualized, including flaws/edge of capabilities.

Ideation, Maintenance, Coding, Testing, Debugging, …

Chapters:

• Speaker Introductions
• 00:03:03 - Personal experiences with AI in coding
• 00:14:41 - Updating regular expression engine
• 00:31:39 - AI Assisting in Code Writing and Fixing Mistakes
• 00:34:01 - AI-Driven Regex Capabilities for Uri Templates
• 00:37:59 - Enhancements in Memory Extensions
• 00:44:10 - Discussion about AI handling tasks and upcoming merge
• 00:46:00 - AI creates and handles test cases automatically
• 00:46:57 - AI tackles project tasks, improves efficiency, and handles edge cases

A good look into how it is and can currently be used.

cross-posted from: https://programming.dev/post/31210046

Firefox 139.0 released yesterday, with support for the Temporal JavaScript API.

I explored the API, writing down the most relevant interfaces into a reference or cheat sheet.

It's certainly and finally a thorough API for handling temporal information. Working with zoned datetime across time offsets and time zones can get very confusing, though.

I love how you can work with them though, especially with durations.

console.log(Temporal.PlainDateTime.from('2025-02-05T08:00:00'))

console.log(Temporal.Now.plainDateTimeISO("Europe/Berlin"))

console.log(Temporal.Now.plainDateTimeISO().add('PT2M0.2S').subtract('PT0.5S').since(Temporal.Now.plainDateTimeISO()))

console.log(Temporal.ZonedDateTime.from('2025-02-05T13:57:35.777888[Europe/Berlin]').withTimeZone('Europe/London'))

Firefox 139.0 released yesterday, with support for the Temporal JavaScript API.

I explored the API, writing down the most relevant interfaces into a reference or cheat sheet.

It's certainly and finally a thorough API for handling temporal information. Working with zoned datetime across time offsets and time zones can get very confusing, though.

I love how you can work with them though, especially with durations.

console.log(Temporal.PlainDateTime.from('2025-02-05T08:00:00'))

console.log(Temporal.Now.plainDateTimeISO("Europe/Berlin"))

console.log(Temporal.Now.plainDateTimeISO().add('PT2M0.2S').subtract('PT0.5S').since(Temporal.Now.plainDateTimeISO()))

console.log(Temporal.ZonedDateTime.from('2025-02-05T13:57:35.777888[Europe/Berlin]').withTimeZone('Europe/London'))

The comment does well in providing context and arguments.

Lets go back to the closest thing we have for requirements for this editor..Default CLI Editor - Feature Exploration!. This discussion was based on the current state of windows and was not concerned with UNIX.

Being a simple text editor, it should not hallucinate, it should not add text one did not type, it should not change the text that was typed. If the user typed a tab character, it was because the user wanted a tab character. If you want four spaces then type four spaces.

edit should by default work like the original namesake and not hallucinate or add characters that were not typed or make assumptions.

Where do you draw the line on "smart" features? Tab should not add indent spaces? Encoding or newline mechanisms? Determining EOF newline?