What would you ask Simon Peyton Jones?

I have long aspired to interview Simon Peyton Jones, whom I consider the most articulate and charismatic figure in the functional programming community. What makes him even more remarkable is his approachability; I reached out to him on LinkedIn—thinking, why not?—and he actually responded. I was so astonished that I initially thought the reply might have come from his son, Michael, whom I occasionally encounter due to my involvement with Cardano and Plutus.

For years, I've dreamed of hosting a podcast where I interview my heroes, blending in crowd-sourced questions alongside my own.

I aim to pose truly insightful questions about the developmental journey of Haskell. I'm uncertain whether I need to center the interview around the publication of his most recent project, Verse, to secure his participation.

Additionally, what areas should I research heavily? I am versed in category theory and functional programming. But, I think I would need to read up on lambda calculus to sufficiently talk about it.

However, I am more inclined to delve into the profound insights he offers on deeper topics, as discussed by other equally eloquent Haskell core developers like Phil Wadler on the CoRecursive podcast. To me, some of the finest podcasting I've ever encountered was an episode where Phil Wadler talks about "God's Programming Language" and reads letters between the pioneers of lambda calculus, at one point remarking that "the laws of programming languages aren't invented; they are discovered."

Another remarkable moment in podcasting was this whirlwind episode with John Wiegley, where he discusses some truly otherworldly research he has conducted.

Answering the question raised at the end of Part 1, we take a look at how a hypothetical Strict Haskell would tie the compilers hands despite pervasive purity. We also examine how laziness permits optimizations that come with no intrinsic cost and compare its benefits to a strict language with opt-in laziness.

Part 1:

• Laziness in Haskell — Part 1: Prologue
Series Playlist:

• Laziness in Haskell

— Contact: • Tweag Website: https://www.tweag.io/ • Tweag Twitter: https://twitter.com/tweagio • Alexis King's Twitter: https://twitter.com/lexi_lambda

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

In the second webinar from our Hackathon series, Fabian Bormann provides an intro into building on Cardano including a list of tools to support you. Next, Mateusz Czeladka discusses how to harness the power of smart contracts with Aiken.

Click the link below to learn more and to register for the Cardano Summit Hackathon. https://summit.cardano.org/hackathon/

In the second webinar from our Hackathon series, Fabian Bormann provides an intro into building on Cardano including a list of tools to support you. Next, Mateusz Czeladka discusses how to harness the power of smart contracts with Aiken.

Click the link below to learn more and to register for the Cardano Summit Hackathon. https://summit.cardano.org/hackathon/

We teach you Haskell

In the past few years, we witnessed the development of multiple smart contract languages - Solidity, Viper, Michelson, Scilla etc. These languages need to enable developers to write correct, predictable behavior smart contract code. Each language development effort therefore ends up spending resources into building formal verification toolsets, compilers, debuggers and other developer tools. In this episode, we are joined by Grigore Rosu, Professor of computer science at UIUC [University of Illinois at Urbana-Champaign] for a deep dive into the K framework. The K framework is mathematic logic and language that enables language developers to formally define all programming languages; such as C, Solidity and JavaScript. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification toolsets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K. This technology has massive implications for smart contract programming language development, and formal verification efforts in the blockchain space. We also cover his efforts to express the Ethereum virtual machine using the K framework, and to develop a new virtual machine technology, called IELE, specifically tailored to the blockchain space. Check out the episode to understand a game changing technology in the formal verification and smart contract safety space.

Topics discussed in this episode:

• Grigore's background with NASA and work on formally verified correct software
• Motivations to develop K framework
• Basic principles behind the operation of K framework
• How K deals with undefined behavior / ambiguities in a language definition
• The intersection of K framework and smart contract technology
• Runtime Verification's collaboration with Cardano
• KEVM and IELE, smart contract virtual machines developed by Runtime Verification
• Broader implications of the K framework for the blockchain industry

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

Back Cover Text

The software development community widely acknowledges that domain modeling is central to software design. Through domain models, software developers are able to express rich functionality and translate it into a software implementation that truly serves the needs of its users. But despite its obvious importance, there are few practical resources that explain how to incorporate effective domain modeling into the software development process.

Domain-Driven Design fills that need. This is not a book about specific technologies. It offers readers a systematic approach to domain-driven design, presenting an extensive set of design best practices, experience-based techniques, and fundamental principles that facilitate the development of software projects facing complex domains. Intertwining design and development practice, this book incorporates numerous examples based on actual projects to illustrate the application of domain-driven design to real-world software development.

Readers learn how to use a domain model to make a complex development effort more focused and dynamic. A core of best practices and standard patterns provides a common language for the development team. A shift in emphasis—refactoring not just the code but the model underlying the code—in combination with the frequent iterations of Agile development leads to deeper insight into domains and enhanced communication between domain expert and programmer. Domain-Driven Design then builds on this foundation, and addresses modeling and design for complex systems and larger organizations.

Specific topics covered include:

• Getting all team members to speak the same language
• Connecting model and implementation more deeply
• Sharpening key distinctions in a model
• Managing the lifecycle of a domain object
• Writing domain code that is safe to combine in elaborate ways
• Making complex code obvious and predictable
• Formulating a domain vision statement
• Distilling the core of a complex domain
• Digging out implicit concepts needed in the model
• Applying analysis patterns
• Relating design patterns to the model
• Maintaining model integrity in a large system
• Dealing with coexisting models on the same project
• Organizing systems with large-scale structures
• Recognizing and responding to modeling breakthroughs

With this book in hand, object-oriented developers, system analysts, and designers will have the guidance they need to organize and focus their work, create rich and useful domain models, and leverage those models into quality, long-lasting software implementations.

This development encodes category theory in Coq, with the primary aim being to allow representation and manipulation of categorical terms, as well realization of those terms in various target categories.

"So the rotary fixture plate is done, right? WRONG. I’ve got just one more feature to add to it. A set of material squaring guides. I have an idea for a dovetail clamp that allows for adjustability, but is also self-squaring. I’ve never seen anything quite like it which could either be a good thing or a bad thing. It’s one of those weird things where the mechanism makes sense, but at the same time… doesn’t. So let’s find out, and build a functional prototype!"

I listen to this (now very old) episode often to get inspired.

When John starts talking about compiling to categories, at around 14:40 to around 30:00, it gets REALLY interesting.

*😁😁 Hoping to bring this kind of discussion to the new Formal Methods community. 😁😁 * Here's the work he talked about: Compiling to categories by Conal Elliott

I need someone to get into the weeds on compiling programs to "axiomatized closed categories". What are the implications? What are the ramifications?

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

Start by reading these two articles:

• https://blog.joinmastodon.org/2023/07/what-to-know-about-threads/
• https://ploum.net/2023-06-23-how-to-kill-decentralised-networks.html

Ok, now that you've done that (hopefully in the order I posted them), I can begin.

I have always been a strong supporter of Open Source Software (OSS), so much so that all of my projects (yes all) are OSS and fully open for anyone to use. And with that, I knew that things could be used for good... and bad. I took that risk. But I also made sure to build stuff that wasn't, in itself, inherently bad. I didn't build anything unethical to my eyes (I understand the nuance here).

But I've seen what unethical devs can do.

Just take a look at those implementing the ModFascismBot for Reddit (that's not its name, but that's what it is). That is an incredibly unethical thing to build. Not because it's a private company controlling what they want their site to do, no, that's fine by me. Reddit can do whatever they want. But because it's an attempt to lie about reality, to force users to do something through manipulation not through honesty. Even subreddits that voted overwhelmingly to shut down still got messaged by the bot telling them that the users (that voted for it) didn't want it and they had to open back up or they would be removed from mod position. This is not ethical. This is not right. This is not what the internet is about.

Or the unethical devs at Twitter, who:

• built in actual keywords to mark Ukraine news as misinformation
• marked Substack as unsafe when they released their own Twitter competitor
• banned Mastodon links for no reason besides the fact that they are a competitor
• marked NPR, BBC, CBC, and PBS as 'state-funded media' even though that is clearly meant to indicate something along the lines of Russia's propaganda arm RT or China Daily, the same for China. Then when there was enormous backlash, they removed the labels, but did the same for the actual government propaganda accounts like RT and China Daily. And then they removed the limits on virality of those posts from those propaganda accounts allowing them to have a massive spike in engagement, thus furthering misinformation.

It's one thing for an organization to have political lean...that is just a part of life, and that will never end. It's another to actually sow disinformation in order to accomplish nefarious things to further your profits. It is what has caused massive addiction to tobacco, the continuation of climate change, death and disfiguration from forever chemicals, ovarian cancer and mesothelioma from undisclosed exposure to asbestos, or selling 'health products' that claim to cure everything under the sun, but can "interfere with clinical lab tests, such as those used to diagnose heart attacks".

Please do not confuse this for saying that companies shouldn't be able to sell things and make a profit. If you want to sell someone something that kills them if they misuse it and you market it as such, you go for it. That's literally how every product in the cleaning aisle of your grocery store works. That's how guns work, that's how fertilizers work, that's why we have labels. But manipulation for profit is unethical, and that's why companies hide it. It hurts their bottom line. They know that their products will not be used if they reveal the truth. Instead of doing something good for humanity, they choose the subterfuge. Profits over people. Profits over Earth honestly. Profits over continuing the human race. Absolutely nothing matters to companies like this. And unethical developers enable this.

---

Facebook (ok, fine, Meta, still going to refer to them as FB though) is trying to join the Fediverse. We as a community, but honestly each of you as individuals, have a decision to make. Do they stay or do they go? Let's put some information on the table.

Facebook...

• lies about the amount of misinformation it removes ^1
• increased censorship of 'anti-state' posts ^1 ^2 ^3
• lied to Congress about social networks polarizing people, while FB's own researchers found that they do ^2
• attempted to attract preteens to the platform (huh, wonder where all that "you must be 13" stuff went) ^4
• rewards outrage and discord ^3

Facebook also...

• Allows for checking on friends and family in disasters ^6
• Created and maintained some of the most popular open source software on the planet (including the software that runs the interface you're looking at right now) [^7][^8]

From my perspective... There's not much good about FB. It has single handedly caused the deaths of tens of thousands of people across the planet, if not hundreds of thousands. It continually makes people angrier and angrier. It's a launching pad for scammers, thieves, malevolent malefactors, manipulators, dictators, to push their conquests onto the world through manipulation, lies, tricks, and deceit. Its algorithms foster an echo chamber effect, exacerbating division and animosity, making civil discourse and mutual understanding all but impossible. Instead of being a platform for connection, it often serves as a catalyst for discord and misinformation. FB's propensity for prioritizing user engagement over factual accuracy has resulted in a global maelstrom of confusion and mistrust. Innocent minds are drawn into this vortex, manipulated by fear and falsehoods, consequently promoting harmful actions and beliefs. Despite its potential to be a tool for good, it is more frequently wielded as a weapon, sharpened by unscrupulous entities exploiting its vast reach and influence. The promise of a globally connected community seems to be overshadowed by its darker realities.

As a person, I believe that we need to choose things as a community. I do not believe in the 'BDFL'...the Benevolent Dictator For Life. Graydon Hoare, creator of Rust, wrote an article just recently about how things would have been different if they had stayed BDFL of Rust. From my position the BDFLs we currently have on this planet really suck. Not just politically, but even in tech. I don't think that path is good for society. It might work in specific circumstances, but it usually fails, and when it does, people get hurt. Badly.

So, with that in mind, I've been working on a polling feature for Lemmy. I seriously doubt I'll be done with it soon, but hopefully FB takes a while longer to implement federation. I understand there's a desire for me, or the other admins to just make a decision, but I really don't like doing that. If it comes down to it, I will implement defederation to start with, but I will still be holding a vote as soon as I can get this damn feature done.

[^8]: the website actually uses Inferno, but from what I can tell it was forked directly from React, judging from the actually documentation and references in the repo.