DEV Community: Adolfo Neto

Type checking is a confession that we’ve created unnecessary complexity

Adolfo Neto — Fri, 05 Sep 2025 17:02:17 +0000

Should we use LLMs?

Adolfo Neto — Thu, 21 Aug 2025 11:52:20 +0000

I was just reading Friends Don't Let Friends Prompt, by Emily M. Bender and I found these arguments against using LLMs quite interesting:

the "theft argument (even though they weren't using it when they would have otherwise paid someone, it's still based on stolen art)"
"the labor exploitation argument (data workers enduring terrible conditions to prevent end users from seeing horrific output)"
"the environmental argument (these things have an environmental cost)"
the expansion argument: "every use of these systems builds the case for training the next one and building the next data center".

What do you think about these arguments?

I will interview Emily and Alex Hanna, the authors of The AI Con, on September 10th, 18:00 (UTC-3).

Unlock Elixir and Erlang with Personalized GPTs from the Erlang Ecosystem Foundation

Adolfo Neto — Wed, 02 Jul 2025 19:00:58 +0000

Hello! As a member of the Erlang Ecosystem Foundation's Education, Training, & Adoption Working Group, I'm want to share a development. For the past few months, Lee Barney, a fellow working group member, has been creating personalized GPTs specifically designed for learning Elixir and Erlang. I'm here to walk you through how you can leverage these powerful tools.

Links to the GPTs here

Accessing the Erlang Ecosystem Foundation GPTs

To get started, head over to chat.openai.com and log in. Once you're in, navigate to the left-hand sidebar. You'll see a "GPTs" option represented by four circles forming a square. Click on that, and then use the "Search GPTs" bar. Type in "Erlang Ecosystem Foundation," and you'll find a selection of specialized GPTs.

Let's explore some of them:

ElixirSparq: If you're a beginner or looking to start your journey with the Elixir language, ElixirSparq is your go-to. You can kick off a chat and ask questions like, "How can I write 'Hello World' in Elixir?" It will provide you with an answer, likely demonstrating something similar to IO.puts("Hello World") within a module.
ErlangSparq: Similarly, for those diving into Erlang, ErlangSparq is designed to guide you through the language fundamentals.
OTPSparq: OTP (Open Telecom Platform) is a crucial library used in both Elixir and Erlang. OTP Spark is your resource for understanding this powerful framework. A great way to begin is by asking, "What is OTP?"

You can easily pin your favorite GPTs to your sidebar for quick access, saving you from searching every time.

New Additions and Learning Strategies

We've recently added two more specialized GPTs:

Erlang DiGraphs User Guide: This GPT is invaluable if you're looking to learn how to use digraphs in Erlang. And remember, what you learn in Erlang regarding digraphs can often be applied in Elixir as well.
Erlang SOFS Users Guide: The Erlang module covered by this GPT deals with sets of sets, finite sets, relations, and sets as first-class native structures. Asking the GPT "What is sets?" will give you a detailed explanation.

I believe that using AI for language learning, especially with these tailored GPTs, can be effective. However, it's crucial to remember that these are learning aids, not substitutes for complete understanding. While you can ask questions, it's generally best to avoid asking the GPT to write entire programs for you. Instead, focus on asking questions that help you understand concepts and guide you toward solutions. Sometimes, you might even need to prompt the system to provide hints rather than full answers.

Of course, these GPTs should complement other learning methods, such as reading books or consulting official language documentation.

A Note on "Miscalculations"

Lee Barney, who developed these GPTs, prefers the term "miscalculation" over "hallucination" when an LLM provides incorrect information. These miscalculations can happen. For instance, a function might be described as taking two arguments when it actually requires three.

This can actually be a beneficial part of the learning process. When such a miscalculation occurs, you'll have to verify the GPT's output. This means you'll have to engage with the language directly – perhaps by testing the code in a Livebook environment for Elixir or in the Erlang terminal. This hands-on verification process helps solidify your understanding and teaches you how to debug and confirm information, which are essential skills for any developer.

Support the Erlang Ecosystem Foundation

The development of these GPTs is just one of many initiatives by the Erlang Ecosystem Foundation. If you appreciate our work and want to support the growth and education around Elixir and Erlang, please consider becoming a sponsor or joining the foundation.

Sponsorship: Companies can become sponsors to help us continue our mission. You can find more information on how to become a sponsor on our website.
Membership: Individuals can also join the foundation. We offer a basic membership (free), an annual supporting membership ($99), and a lifetime supporting membership ($999).

Click here to join!

Thank you for your time, and we look forward to seeing you contribute to the Erlang and Elixir communities!

Lean won the SIGPLAN Programming Languages Software Award 2025

Adolfo Neto — Thu, 19 Jun 2025 18:54:24 +0000

Great news!!!

Lean won the "SIGPLAN Programming Languages Software Award 2025". SIGPLAN is The ACM Special Interest Group on Programming Languages.

Congrats to Leonardo de Moura 🇧🇷, the Lean FRO team and the Lean community!!!

About the Award

The SIGPLAN Programming Languages Software Award is given by ACM SIGPLAN "to an institution or individual(s) to recognize the development of a software system that has had a significant impact on programming language research, implementations, and tools. The impact may be reflected in the widespread adoption of the system or its underlying concepts, by the wider programming language community either in research projects, in the open-source community, or commercially. The award includes a prize of $2,500."

The committee for this year was composed of: Niki Vazou, IMDEA (co-chair); Alexandra Silva (co-chair); Andrew Myers (observer); David Grove, IBM Research (SPLASH); Alastair Donaldson, Imperial (PLDI); Xavier Leroy, Inria (ICFP); and Amal Ahmed, Northeastern U (POPL).

The award was presented to

Gabriel Ebner
Soonho Kong
Leo de Moura
Sebastian Ullrich

The award slide reads:

"Citation: The Lean theorem prover is a remarkable software artifact. Grounded on strong theoretical and engineering foundations, Lean has had and continues to have a broad impact on industrial practice and scientific research. In particular, the Lean project has already had a significant impact on mathematics, hardware and software verification, and AI. It has gained substantial traction in the mathematics community with a user-developed library, Mathlib, that has more than 1.8M lines of code. The verification of foundational results at the request of Fields Medalist Peter Scholze and the verification of the Polynomial Freiman–Ruzsa Conjecture led by Fields Medalist Terence Tao have earned the system widespread recognition. It is clear that formal methods based on Lean will play a central role in mathematics in the years to come. Lean is also used in important verification projects in industry, including the verification of the Cedar access control language at AWS, the verification of the SampCert sampler for differential privacy at AWS, and blockchain verification projects at companies like StarkWare and Nethermind. Finally, with the success of projects like DeepMind’s AlphaProof and the adoption of Lean by startup companies like Harmonic, Lean has become the de facto choice for AI-based systems of mathematical reasoning."

PLDI'25 Award Ceremony

You can watch the award being presented at 9:22:58 in the "PLDI'25 Award Ceremony (June 19th)" livestream:

Leonardo de Moura's talk at PLDI

Before the award ceremony, Lean's Chief Architect Leonardo de Moura gave a keynote talk at the 46th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2025) in Seoul. His talk, titled "Lean: Machine-Checked Mathematics and Verified Programming, Past and Future," begins at 55:31 of the livestream:

Previous Winners

Who has won this award before?

Rust
OCaml
Scala
Racket
GCC
Coq
Glasgow Haskell Compiler
LLVM Compiler Infrastructure

And Leo had already won it before with the Z3 theorem prover.

Leonardo de Moura interviews

In English

Type Theory for All, by Pedro Abreu

Building Better Systems

In Portuguese

I have interviewed Leonardo twice.

Fronteiras da Engenharia de Software

Professor Adolfo Neto

Lean introduction talk

As part of the Esquenta SE4FP series, there will be an online talk in Portuguese by Sofia Rodrigues on the Lean programming language and theorem prover. Sofia is a Research Software Engineer at Lean FRO. The talk takes place on Wednesday, June 25, 2025, at 4:00 PM (UTC-3). The registration form is available at: https://forms.gle/gXQyGLeMKmDHfhSb8.

A Bluesky post

"LEAN won the award for programming language software :)" at PLDI'25, told me Sofia Rodrigues!!!
@lean-lang.org #LeanLang #LeanProver #Lean4

🥳🎉🇧🇷🎊🍺

[image or embed]
— Adolfo Neto (@adolfont.github.io) June 19, 2025 at 2:08 PM

The Elixir Pipe Operator

Adolfo Neto — Sun, 15 Jun 2025 17:54:09 +0000

The Elixir pipe operator (|>) is beautiful.

How do you use it? Imagine you have a data structure and two or more functions that transform it in sequence.

Suppose you have a Numbers module in a file called numbers.ex:

defmodule Numbers do

  def filter_even_numbers(list) do
    Enum.filter(list, fn x -> rem(x, 2) == 0 end)
  end

  def double(list) do
    Enum.map(list, fn x -> x * 2 end)
  end

end

Then, open an Interactive Elixir session:

$ iex numbers.ex

Now, if you copy and paste this into your iex session:

iex> [1, 2, 3, 4, 5, 6]
|> Numbers.filter_even_numbers()
|> Numbers.double()

You’ll get:

[4, 8, 12]

Some say the pipe operator came from F#. I once asked José Valim, and he said he doesn't remember exactly where the idea came from. But it’s true that F# had pipe operators—more than one kind—before Elixir.

Want to go deeper into the pipe operator? Check out this excellent blog post by João Paulo Abreu: Learning Elixir: Pipe Operator. Don’t miss the “Further Reading” section.

And if you're looking for a course on functional programming, check the post below:

My "Introduction to Functional Programming" course will be fully remote.
Classes are expected to begin in early August.
Mondays, 15h50-18h40 (UTC-3).

Interested in joining? Please fill out the form to express your interest. You will be notified when enrollment opens.

bit.ly/IFP_2025

[image or embed]
— Adolfo Neto (@adolfont.github.io) June 13, 2025 at 8:49 AM

Who's Still Podcasting About Elixir? (May 2025 Edition)

Adolfo Neto — Fri, 23 May 2025 13:54:11 +0000

I am writing this post on May 23, 2025.

First, let me define what I mean by an active podcast: one that has released at least one episode in the past 90 days.

Second, by an Elixir podcast, I mean a podcast that is related to the Elixir programming language or the BEAM ecosystem, and that features many episodes focused on Elixir.

As of today, to the best of my knowledge, there are four active Elixir podcasts:

Thinking Elixir. The latest episode was "254 - Lua Scripting and Tidewave on Zed", published on May 20, 2025.
Elixir Mentor. Latest episode: "49 - Elliot Clark in Simplifying Cloud Infrastructure", published on May 17, 2025.
Elixir em Foco (in Portuguese) — Latest episode: "50 - Refactorex: Refatoração em Elixir, com Gabriel Pereira", published on May 7, 2025.
BEAM Radio. Latest episode: "90 - Josh Price: Ash and the Greater Elixir Community", published on April 22, 2025.

Do you know of any other Elixir podcasts that have released episodes in the past three months?

The original motivation for creating Lean was software verification

Adolfo Neto — Sun, 18 May 2025 13:53:19 +0000

"The main motivation, the original motivation for (creating) Lean was in software verification, right? I mean, Z3 was very popular at bug finding, for bug finding at Microsoft, was very influential there. But (for) Lean the goal was, can we make the same, have the same success of software verification?

We went to a very strange path. I mean, having impact in mathematics that we never dreamt of.

But the goal in both cases is like we, both in software mathematics and in AI, today rely on manual review, partial testing. A mistake in a theorem can be catastrophic, invalidating the whole result. The same thing (happens) for a critical piece of software, right? And one thing I see all the time, people fearing to make a change a piece of software because they fear by making the change they may be introducing a bug, especially if it's a critical piece of software."

Watch more in the video below and in the full talk at the following link:

From "Leo De Moura: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI"

Next Fronteiras Interview: Daniel Feitosa on Technical Debt Management

Adolfo Neto — Mon, 05 May 2025 12:36:28 +0000

Next week, on May 12th, 2025, we are going to interview Daniel Feitosa, a Brazilian Software Engineering professor at the Faculty of Science and Engineering, University of Groningen.

When I write "we," I mean the Frontiers of Software Engineering podcast, which is in Portuguese. I would love to have something like it in English, but as far as I know, there is no podcast that regularly interviews Software Engineering professors and researchers to discuss their work and publications.

We always ask our interviewees what they would like to talk about, and Daniel chose Technical Debt Management. It's a very important topic in practice for software engineering professionals, isn't it?

We also ask our interviewees to share 2 to 4 publications, and these are the ones Daniel sent us:

C. Zhong, D. Feitosa, P. Avgeriou, H. Huang, Y. Li, H. Zhang. PairSmell: A Novel Perspective Inspecting Software Modular Structure. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE '25), 2025. Distinguished Paper Award. https://arxiv.org/abs/2411.01012
J.P. Biazotto, D. Feitosa, P. Avgeriou, E.Y. Nakagawa. Automating Technical Debt Management: Insights from Practitioner Discussions in Stack Exchange. In Proceedings of the 8th ACM/IEEE International Conference on Technical Debt (TechDebt '25).
J.P. Biazotto, D. Feitosa, P. Avgeriou, E.Y. Nakagawa. Technical Debt Management Automation: State of the Art and Future Perspectives. Information and Software Technology, 167:107375, 2024. https://doi.org/10.1016/j.infsof.2023.107375
J. Tan, D. Feitosa, P. Avgeriou. The Lifecycle of Technical Debt that Manifests in Both Source Code and Issue Trackers. Information and Software Technology, 159:107216, 2023. https://doi.org/10.1016/j.infsof.2023.107216

If you want to watch or listen to our episodes, check out https://www.youtube.com/@fronteirases.

On YouTube, you can enable automatic translations to view subtitles in English.

Let me know if you'd like a version adapted for social media or a blog format.

Tidewave: Connecting Web Apps to AI-Powered Development

Adolfo Neto — Wed, 30 Apr 2025 11:01:57 +0000

José Valim recently introduced Tidewave, a new tool designed to connect web applications with editors and AI agents such as Claude, Zed, Cursor, Windsurf, and others.

Tidewave works by embedding a Model Context Protocol server into a running web application. This allows development tools—not just to analyze code statically—but to observe and introspect applications at runtime, enabling much smarter and more helpful interactions during development.

The project is open source and currently supports Phoenix and Rails, with additional frameworks planned for the future.

A Live Demo: Adding Pricing Plans with AI

// Detect dark theme var iframe = document.getElementById('tweet-1917296901268910405-183'); if (document.body.className.includes('dark-theme')) { iframe.src = "https://platform.twitter.com/embed/Tweet.html?id=1917296901268910405&theme=dark" }
In a demonstration, Valim showcased Tidewave in action using a freshly generated Phoenix application. After setting up basic authentication and a settings page, he outlined a common task for SaaS applications: adding pricing plans.

To accomplish this, he used Claude Desktop—a standard AI interface. While Claude itself isn’t a dedicated coding agent, when paired with Tidewave, it effectively becomes one.

The prompt given to the AI was:

“I'm building a SaaS. Please add a price selector with common options to the live view page I'm currently looking at. Once you're done with the changes, run mix compile in the shell to make sure everything is working, and fix it if it's not.”

Thanks to Tidewave, the AI was able to:

List project files,
Detect which page the user was viewing (DemoWeb.UserLive.Settings),
Retrieve contextual code information,
Edit the correct files.

Even when errors were introduced (like invalid syntax), Tidewave enabled the AI to compile the project, detect issues, and attempt automatic fixes. Eventually, the application reloaded with a functioning pricing selector—a solid foundation for subscription plan logic.

The Takeaway

This demonstration wasn’t just about automating code edits—it showed that with Tidewave, even general-purpose AI tools like Claude can behave like intelligent coding assistants when given runtime context.

The key message: whether using Claude, Cursor, or other tools, Tidewave enhances their capabilities by exposing real-time insight into your application, enabling faster, smarter development.

The demo closed with a reminder: what was shown was just the beginning. Developers can continue using the AI to expand features—like integrating Stripe or connecting to a database—or take over from where the AI left off.

Tidewave is available today, open source, and growing. It's a glimpse into the future of software development—where AI and runtime context work hand-in-hand.

Do you use LLMs? And some podcast recommendations

Adolfo Neto — Fri, 04 Apr 2025 16:30:06 +0000

Right now, I am using LLMs to (a few examples):

Translation
Given the transcript and/or script of an episode of my podcasts, generate a summary (show notes) for the episode
Generate fluffy or bureaucratic text, filler text, based on a few main points
Give me the main points of a text—but from a text I don’t need to read. This is not a replacement for a full reading. If the LLM didn’t exist, I simply wouldn’t read it.
Ask questions in the classroom (I am a professor) just to see a summary of a topic and, perhaps, find some information I had forgotten—or, even better, a hallucination.
Manipulations with copied texts from web pages. For example, suppose I copy something from the internet, and it comes with a lot of clutter. I ask the LLM to remove the clutter.
Transcribe text from images to use as ALT on Bluesky. I mostly use Mistral Le Chat for this.
Generate programming exercises.

And more...

I am NOT using them to:

generate images (unless as a capability test)
write blog posts for me (I did it a few times and the results were not great)

Podcast Suggestions

If you're using LLMs, I recommend listening to the following podcasts:

I've listened to a few episodes of both, and they're excellent.

I know there's another related podcast, but I haven't listened to any of its episodes yet:

Mystery AI Hype Theater 3000

One of its hosts is Emily M. Bender, the first author of the well-known paper:

On the Dangers of Stochastic Parrots: Can Language Models Be Too Big? 🦜

Feedback

And you? What are you using LLMs for? What are you not using them for?

Unsafe Impedance: Safe Languages and Safe by Design Software, by Lee Barney and Adolfo Neto

Adolfo Neto — Sat, 02 Nov 2024 15:25:45 +0000

Arxiv++ AI-Generated Summary

Arxiv link for Unsafe Impedance: Safe Languages and Safe by Design Software, by Lee Barney and Adolfo Neto

Problem Statement

This paper addresses the insufficiency of merely declaring programming languages as "memory safe" for achieving secure software. The paper argues that while such declarations are necessary, they fail to address the ease with which unsafe code can be written and integrated, leading to vulnerabilities.

Main Claims

The concept of "unsafe impedance" is introduced as a novel perspective for evaluating language safety in the context of software security. Unsafe impedance refers to the difficulty programmers experience when complying with language restrictions on writing unsafe code.
A "Secure by Default" language is defined as one that protects against the production of all Common Vulnerability and Exposures (CVEs), particularly memory-related CVEs.
While languages like C#, Go, Java, Python, Rust, and Swift are declared memory safe, they all allow unsafe code to be written or loaded from libraries, making them "unsecure by default."
Erlang and Elixir, two BEAM languages, are considered "secure by default" due to their functional nature, immutability, and lack of pointer manipulation capabilities. However, they also allow the integration of "Native Implemented Functions" (NIFs) that can introduce unsafe code.
The paper proposes an "Unsafe Acceptance Process" (UAP) as a business process to enhance software security. UAPs impose a significant barrier to the loading and use of potentially unsafe code, aiming to increase unsafe impedance.

Methodology

The paper analyzes nine commonly used programming languages (C#, Go, Java, Python, Rust, Swift, Erlang, Elixir, and C/C++) by providing examples of how unsafe code can be written or loaded in each language. The authors evaluate the level of unsafe impedance present in each language based on the syntactical and procedural hurdles required to write or use unsafe code.

Key Results

The study finds that none of the languages declared memory safe in cybersecurity documents are truly "secure by default," as they allow unsafe code to be incorporated.
Erlang and Elixir are categorized as "secure by default" languages due to their functional nature and lack of native unsafe code capabilities. However, the authors highlight the potential for introducing unsafe code through NIFs, emphasizing the need for strong security measures.
The paper proposes an "Unsafe Acceptance Process" (UAP) as a strategy for organizations to mitigate risks associated with unsafe code, especially in languages like Erlang and Elixir, which are susceptible to vulnerabilities introduced by NIFs.

Behind the Code: Highlights from Elixir Curitiba 2024 and Future Visions

Adolfo Neto — Thu, 31 Oct 2024 12:09:23 +0000

Organizing and participating in Elixir Curitiba 2024 was an enriching experience, and I’d like to share some behind-the-scenes details about the event. From the start, I explored various venue options but ultimately chose Trio Pagamentos for its logistical convenience. Unlike larger events like Code BEAM or Elixir Conf, I opted to keep things simple and free, which I see as a unique feature for our community. For future editions, I’m considering gathering more participant information to streamline the registration process.

As for organization and outreach, we had the Elixir CWB community on Telegram, Elixir Curitiba on WhatsApp, and a basic website on GitHub. Trio Pagamentos, the event’s venue, and the organizing team were essential in making everything happen. The program covered a variety of topics, from women in STEM to using Elixir. Highlights included Larissa Behrens Soares’s talk on competitive programming focused on women, David Alencar’s session on Elixir development, Julia Mathias’s presentation on , and Kelvin Stinghen’s engaging performance with live coding and juggling.

We had a few last-minute schedule adjustments, such as moving David’s talk up to accommodate an unplanned break. Though we didn’t officially announce a coffee break, attendees appreciated it, and we had semi-professional photographer Gustavo Arcoverde capturing moments throughout. Julia Mathias’s participation, representing Turn.io, was another highlight, and her presence significantly contributed to the event’s success.

One of the most memorable moments was Kelvin’s juggling performance, drawing an analogy between the balls’ positions and running processes—perfectly capturing the event’s essence. Julia’s presentation also stood out; she works remotely from Rio de Janeiro for a South African company, setting up WhatsApp chat systems.

We wrapped up with a final coffee break and a raffle for a programming book on Lua, reinforcing the spirit of learning and camaraderie that defined the event. Looking ahead, I invite everyone to consider joining Elixir Curitiba 2025 and collaborating in the organization, keeping the event free and accessible. I’m also planning an Elixir event in Maceió and am open to new ideas to strengthen our community.

Video in Portuguese: