Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
det.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Mastodon Server des Unterhaltungsfernsehen Ehrenfeld zum dezentralen Diskurs.

Administered by:

Server stats:

1.9K
active users

det.social: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.2

#softwareengineering

13 posts11 participants0 posts today
Public
SnackTraces

New to programming/software development?

Can I help?

I can walk us through using git, a popular source control tool. I can demo how use an IDE (integrated development environment) for debugging and writing code.

Live, now and for next 3 hours from this post. DM me.

Over 20 years experience here and wanting to give back. Free, just wanting to lessen the ick in the world.

#programming#techNewbie#softwareengineering
Public
Louis Ingenthron

Please boost for reach! Which would you prefer from a self-funded indie game studio that can't afford translation services:

1) Don't translate the game at all. Just leave it in English.
2) Use LLMs to translate the games, but have a crowdsourcing system to correct errors.
3) Have a crowdsourcing system and only make languages available when the crowd completes them.

· 45 people · Closed
#GameDev#IndieDev#GameDevelopment
Public
Richard Donovan

Are you struggling to retain new information?

Sleep plays a crucial role in transferring short-term memory to long-term memory, which is essential for learning new skills.

Make sure you get 7-9 hours of sleep to improve your memory and learning abilities.

Here are my top tips for better sleep?

👉 Earplugs
👉 A good quality mattress
👉 A well-fitting sleep mask
#developers #coding #softwaredevelopment #softwareengineering #wellbeing #mindset #mentalhealth

Public
Hacker News

Teaching Program Verification in Dafny at Amazon (2023)

dafny.org/blog/2023/12/15/teac

#HackerNews #TeachingProgramVerification #Dafny #Amazon #2023 #SoftwareEngineering #CodeQuality

Dafny Blog · Teaching Program Verification in Dafny at AmazonIntroduction We recently made available some teaching material that we have used to teach program verification to scientists and engineers at Amazon. It composed of lecture slides and exercises with solution. If you want to learn about Dafny and program verification, you can jump right in. You will learn how to program in Dafny, how to do use Dafny as a proof assistant, and finally how to verify programs. If instead you are more interested in teaching program verification, you may find the organization of the lectures and the focus on Dafny as a proof assistant surprising, and the following note should provide some context and explanations. Dafny: Program Verifier and Proof Assistant A proof plays two roles. (i) A proof convinces the reader that the statement is correct. (ii) A proof explains why the statement is correct. The first point consists of the administrative (‘bookkeeper’) activities of verifying the correctness of the small reasoning steps and see if they constitute a correct proof. One doesn’t have to look at the broad picture, but one just has to verify step by step whether every step is correct. The second point deals with giving the intuition of the theorem: Why is it so natural that this property holds? How did we come to the idea of proving it in this way?    — Herman Geuvers, in Proof assistants: History, ideas and future One way to introduce program verification, including writing specifications and proofs, is exemplified by the book Program Proofs authored by K. Rustan M. Leino and published by MIT press. A defining characteristic of the methodology in that book is that verification is not only always motivated by programs, but specifications and proofs are attributes of programs. The book starts by considering simple imperative programs whose specification is written as pre and post conditions, and proving is done by writing annotations for loops and, on occasion, additional assertions. The curriculum continues with programs of increasing complexity, and specification and proofs continue to “decorate” programs. The concept of a proof is introduced somewhat implicitly through a program logic that details the effect of different programming constructs on the validity of a specification. This is an effective way to teach program verification: combined with Dafny's automation, one can verify programs by decorating them with a few assertions that explain at a high-level why the specification should hold. It promotes a style of program verification where “proving” amounts to explaining. Unfortunately, when automation comes short, it may not always be clear what explanations will help with the verification. It may seem as if one needs to provide the right assertion at the right place, without a clear methodology to figure it out. This can be frustrating to a developer for whom program verification, after appearing so simple for a while, may now seem ad hoc. We attempt to address this problem by providing a complementary perspective on program verification in Dafny. The key idea is to introduce Dafny as a proof assistant and to study proofs explicitly and independently of programs. With this perspective, we not only learn how to write intuitive proofs that take advantage of automation, but we also learn to write detailed formal proofs in natural deduction. This methodology opens the possibility of proving by convincing: a handful of rules can be used to refine a proof that will eventually pass the verification if it is indeed valid. The course is organized in 3 distinct parts. In the first two, Dafny is in turn introduced as a programming language (with no verification) and as a proof assistant (with no programming). Program verification is introduced last and emphasizes extrinsic verification. Part 1: Dafny as a Programming Language The first set of lectures introduces Dafny as a programming language, without any consideration for verification. The primary motivation is to allow Dafny newcomers to familiarize themselves with the syntax and semantics of the language, and its tools (CLI, IDE). It also makes it easy for more seasoned Dafny developers to skip directly to verification. Finally, it emphasizes that Dafny is at its core a full-fledged and classic programming language with strong static typing, object-orientation, and functional features. It may be an opportunity to introduce Dafny's foreign function interface and the idea that Dafny can be used as part of a large software project. We introduce in turn functional programming, imperative programming, and object-oriented programming. We usually keep the presentation of the module system to a minimum. Part 2: Dafny as a Proof Assistant After introducing Dafny as a programming language while ignoring verification, we learn about Dafny as a proof assistant while ignoring programming. We start by introducing the language of specification of Dafny. At its core, a Dafny specification is composed of uninterpreted symbols of type, constant, predicate, and function symbols and the language of formulas is a variant of Church's simple type theory or higher-order logic. The lecture also introduces lemma as a way to declare a family of formulas and axiomatize the meaning of symbols. In particular, the primitive types and operations such as reals or sets are presented as specific theories. We then explain how to define types, constants, predicates, and functions instead of axiomatizing them and assuming their existence. This is an opportunity to talk about partiality, termination of functions, fixed-points, and algebraic datatypes. Finally, we start studying proofs in Dafny in the more intuitive way that aims to prove by explaining. In this style, which is the more idiomatic Dafny style of proofs, one can prove in a way that is similar to the kind of proofs that we write in a high-school geometry class by making intermediate assertions, appealing to know results, fixing values and assumptions (e,g, let x be a fixed but arbitrary odd number), and high-level proof methods such as proof by contradiction, proof by case analysis, or proof by induction. Lastly, and most importantly, we study proofs in a much more formal way by explaining how to develop completely detailed and rigorous proofs using the rules of natural deduction (and sequent calculus). This systematic approach to formal proofs in Dafny allows one to prove by convincing, with the fundamental idea that you can always provide enough details so that the verifier will eventually accept your proof if it is indeed valid. Part 3: Program Verification in Dafny As we mentioned in the introduction, a typical path to learning about program verification in a language like Dafny would be to start with simple imperative programs, specifications as program annotations, and proofs as program annotations in a program logic. However, since we introduced proofs independently of programs by taking the unusual point of view that Dafny is a proof assistant and that proofs are expressed in natural deduction, our journey into program verification is somewhat different. We start with verification of functional programs, as it is largely similar to verifying mathematics. More specially, we first review extrinsic verification of functional programs, meaning that we keep function and type definitions separate (as much as possible) from specifying and proving their properties. In practice, it means that we do not annotate functions with properties but instead state and prove them as separate lemmas. Only then do we go over intrinsic verification of functional programs with pre and post conditions, and subset types. The motivation for keeping extrinsic and intrinsic verification separate is to emphasize the importance of being mindful about proof brittleness and that it may be a better strategy in general to introduce intrinsic verification where it simplifies verification the most, rather than making it the default verified programming strategy. We then discuss verification of imperative programs. First, we introduce local state and finally mention briefly program logic, loop invariants, and ghost state. We also emphasize an important methodology where instead of proving properties of an imperative program directly, one first proves that it behaves as a functional model and then prove interesting properties on that functional model. Finally, we talk about verification of object-oriented programs. The material is standard, but we emphasize the importance of defining an object's API by writing clients first to avoid coming up with an API that is inconsistent or cannot actually be used. We also emphasize that ghost representations need not be limited to sets and that it is tremendously useful to capture as much as possible the intended structure of a class in the type of its representation. Lastly, we emphasize the importance of master nodes in data structures that can make verification significantly easier. Conclusion The first version of this course was designed as a complement to Program Proofs. Its goal was to introduce seasoned Dafny software engineers to a different way of thinking about proofs by introducing them to some of the material from a course on the foundations of proof systems ; natural deduction and sequent calculus in particular. There is anecdotal evidence that it was effective and we have continued to develop this curriculum to use it both as an introduction to program verification, and as a way to help experts take their proving skills to the next level. Automation can be a significant challenge to teaching formal proofs in Dafny because it makes it difficult to work on simple examples and exercises, but the lecture on proving by convincing shows one attempt to do so.
Public *
Tom

After 6 months of heavy-use and evaluation of AI coding assistants, I've gone back to a non-AI neovim and VSCode setup. Even after a week I feel more productive. I've learned a few topics deeply by reading docs, didn't feel like I was wasting time going in circles and it honestly feels like a weight off my shoulders.

I've also learned where the checks and balances need to be in our CI system to mitigate work that may be written in part by AI tools.

I can't see any future in using AI to write code. Due to the nature of LLMs, it's never going to be able to produce code that doesn't require as much time to review as it does to write by hand.

I still occasionally use ChatGPT to ask questions but I've noticed my usage of DuckDuckGo has returned to almost normal levels too as a side effect.

I have to do these things as part of my job is to guide and advise our engineering teams. I need to be in a position to talk about these things from a perspective of experience. But it's been a tough 6 months. Glad it's over.

#ai#llm#software
Public *
Pol Dellaiera

Le Replay est disponible :-)

videos.univ-grenoble-alpes.fr/

Dans cette présentation, nous discuterons de reproductibilité dans le contexte d’environnements de développement modernes, en nous appuyant sur une expérience concrète au sein de la Commission Européenne. Je partagerai mon parcours, les leçons tirées de mon mémoire de master, et comment des outils comme Nix peuvent radicalement transformer les pratiques de développement, en rendant les environnements plus fiables, plus transparents et plus collaboratifs. Une presentation à la croisée de l’open source et de l’ingénierie logicielle.

Merci @reproductible_fr !

Sources disponibles @ recherche-reproductible.fr/pas

recherche_reproductible_dellaiera_nix.mp4
PODrecherche_reproductible_dellaiera_nix.mp4Séminaire du réseau Recherche Reproductible Reproductibilité et environnements de développement May 23, 2025 Dans cette présentation, nous discuterons de reproductibilité dans le contexte d’environnements de développement modernes, en nous appuyant … Added by: Céline Acary-Robert
#nix#softwareengineering
Public
Hacker News

Automated Verification of Monotonic Data Structure Traversals in C

arxiv.org/abs/2505.18818

arXiv logo
arXiv.orgAutomated Verification of Monotonic Data Structure Traversals in CBespoke data structure operations are common in real-world C code. We identify one common subclass, monotonic data structure traversals (MDSTs), that iterate monotonically through the structure. For example, strlen iterates from start to end of a character array until a null byte is found, and a binary search tree insert iterates from the tree root towards a leaf. We describe a new automated verification tool, Shrinker, to verify MDSTs written in C. Shrinker uses a new program analysis strategy called scapegoating size descent, which is designed to take advantage of the fact that many MDSTs produce very similar traces when executed on an input (e.g., some large list) as when executed on a 'shrunk' version of the input (e.g., the same list but with its first element deleted). We introduce a new benchmark set containing over one hundred instances proving correctness, equivalence, and memory safety properties of dozens of MDSTs found in major C codebases including Linux, NetBSD, OpenBSD, QEMU, Git, and Musl. Shrinker significantly increases the number of monotonic string and list traversals that can be verified vs. a portfolio of state-of-the-art tools.
#HackerNews#AutomatedVerification#MonotonicDataStructures
Public
Reinhard Lackner

Just to be on record:
I honestly didn’t expect that even non-YAML code (👀 @nuke build – yeah, I’m talking to you...) would require just as many fucking never-ending commits.
Azure DevOps has proven me wrong. (lol)

The real pain point?
No local test run
No Run pipeline locally
Zero feedback until you PR, merge, and let it rip on main

So yeah, we’re basically testing on the main branch. In production. In 2025.
For everything else, there’s: ¯\_(ツ)_/¯

Also, I firmly believe that not only Carthage must be destroyed, but also:

- CI/CD with no local feedback loop
- “Works on my machine” excuses
_ YAML files that silently break on pasted tabs
- And every doc that starts with “just”

And yes — I really thought nuke build would make things better...
But after 24 hours of commits, checks, and trial-and-error, I’ve been proven otherwise (and I really wanted to make it work and local debugging is awesome — but it’s useless when the docs are a soggy mess and don’t reflect reality.)

#DevOps #AzureDevOps #YAML #NukeBuild #CI #CICD #MainBranchDrivenDevelopment
#WorksOnMyMachine #AgileStruggles #ModernDev #CarthagoDelendaEst #DevHumor
#BuildFail #DebuggingHell #LocalIsNotProd #SoftwareEngineering #DotNet #DevLife

ExploreLive feeds
About