jorgegalindo

We open-sourced lean4-markdown, a typed Lean 4 library for building Markdown documents programmatically. The idea is straightforward: if you're generating verification reports or audit traces in Lean 4, you want the document structure checked by the same type system as the rest of your code. Ill-formed Markdown becomes a type error rather than a runtime surprise. This is part of a small ecosystem we're building around Lean 4 as a general-purpose platform, alongside lean4-flow and lean4-json-schema. Happy to answer questions about design tradeoffs.

Hey HN,

We wrote about something we keep thinking about: the gap between code that runs and code that's provably correct.

The post walks through a simple Java banking app with three bugs that compilation won't catch, tests are unlikely to catch, and an LLM reviewing the code would almost certainly miss. The most interesting one is structural: LLMs reason within a context window, but the most dangerous bugs are global properties that cross component boundaries. The preservation of money in a transfer isn't a property of withdraw() or deposit() in isolation.

Curious whether others have run into this class of problem in production.

We’ve been working on a software verification platform designed for AI-generated code. As code assistants accelerate development, verification becomes the bottleneck.

In this post, we outline the core principles we’re using to design a trustworthy verification system:

• Explicitly model semantics when possible • Make approximations and assumptions visible • Avoid confident false positives and false negatives • Surface uncertainty instead of hiding it

Our main idea is that trustworthiness isn’t about absolute certainty. It’s about being explicit about assumptions and limitations so engineers can make informed decisions.

Would love feedback from people working on formal methods, static analysis, or AI-assisted development.

Author here . This isn’t meant as advice or a productivity framework. It’s just a personal reflection on how becoming a parent changed the constraints around my time while building a startup.

Writing it after talking with a founder friend who just had a baby and felt he was failing at both work and parenting. Sharing in case it resonates with others in a similar situation. Happy to answer questions or clarify anything.

I’ve been building startups for years and became a parent along the way. For a long time, I thought having kids would hurt my productivity. What actually happened is that it forced me to take time seriously.

This isn’t a guide or advice. It’s just my personal experience on how parenting changed how I prioritize, say no, use my calendar, and think about work. Writing it down after a conversation with a founder friend who just became a parent.

Sharing in case it’s useful to someone in a similar situation.

This is the story of how I turned my passion for discovering records into onerecord.club, Spain’s first indie vinyl subscription service.

In the article, I share the steps I took to transform a hobby into a tangible product: finding the right idea, teaming up with the right people, and navigating the challenges of launching something new.

If you're curious about how to turn what you love into something others can enjoy too, check it out! I'd love to hear your take on turning hobbies into products.

I recently took a step back from my career to go on a sabbatical, and it’s been a surprising journey—both liberating and challenging in ways I didn’t expect.

In my latest blog post, I share what I’ve discovered about how time, priorities, and creativity shift when you’re no longer tied to the grind. This might resonate with you if you’ve ever thought about taking a sabbatical (or just wondered what it’s like).

I would love to hear your thoughts or experiences if you’ve been through something similar!

I share the key challenges I faced scaling my company from 4 to +100 employees and what I learned from the mistakes along the way.