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

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.

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?

Here's the conclusion of the paper Wadler is referring to in this interview:

Proposition as Types informs our view of the universality of certain programming languages. The Pioneer spaceship contains a plaque designed to communicate with aliens, if any should ever intercept it. They may find some parts of it easier to interpret than others. A radial diagram shows the distance of fourteen pulsars and the centre of the galaxy from Sol. Aliens are likely to determine that the length of each line is proportional to the distances to each body. Another diagram shows humans in front of a silhouette of Pioneer. If Star Trek gives an accurate conception of alien species, they may respond “They look just like us, except they lack pubic hair.” However, if the aliens’s perceptual system differs greatly from our own, they may be unable to decipher these squiggles. What would happen if we tried to communicate with aliens by transmitting a computer program? In the movie Independence Day, the heroes destroy the invading alien mother ship by infecting it with a computer virus. Close inspection of the transmitted program shows it contains curly braces—it is written in a dialect of C! It is unlikely that alien species would program in C, and unclear that aliens could decipher a program written in C if presented with one. What about lambda calculus? Propositions as Types tell us that lambda calculus is isomorphic to natural deduction. It seems difficult to conceive of alien beings that do not know the fundamentals of logic, and we might expect the problem of deciphering a program written in lambda calculus to be closer to the problem of understanding the radial diagram of pulsars than that of understanding the image of a man and a woman on the Pioneer plaque. We might be tempted to conclude that lambda calculus is universal, but first let’s ponder the suitability of the word ‘universal’. These days the multiple worlds interpretation of quantum physics is widely accepted. Scientists imagine that in different universes one might encounter different fundamental constants, such as the strength of gravity or the Planck constant. But easy as it may be to imagine a universe where gravity differs, it is difficult to conceive of a universe where fundamental rules of logic fail to apply. Natural deduction, and hence lambda calculus, should not only be known by aliens throughout our universe, but also throughout others. So we may conclude it would be a mistake to characterise lambda calculus as a universal language, because calling it universal would be too limiting.