Après NVidia, c'est Zenseact, une startup issue de Volvo qui fournit des logiciels pour voitures autonomes, qui choisit Spark pour ses développements.

Nous, on trouve que c'est une bonne idée :)

https://www.just-auto.com/sponsored/meeting-asil-c-and-d-with-formal-methods/

#spark #ada #adalanguage #formal_methods

неприятно болеть.

Одновременно, за счёт некоторого упоротства, удалось поизучать пару вещей.

Наткнулся и потыкал очень простой верификатор теорем Acorn[1]. Оно прикольное, оно простое, оно тупое (там не очень большая база готовых теорем, и, по ощущениям, оно ещё и немного тупит). Возможно также плюс - что есть плагин для VS Code. Код на acorn выглядит примерно так:

```acorn
theorem threeven_plus_three(n: Nat) {
threeven(n) implies threeven(n + 3)
} by {
let d: Nat satisfy {
3 * d = n
}
3 * (d + 1) = n + 3
}
```
A implies B - из A следует B,
threeven - функция (Nat) -> Bool, определённая ранее,
переменная n: Nat - произвольное натуральное число.

Здесь доказывается, что если n делится на 3 без остатка, то и n+3 делится на 3 без остатка.

К сожалению, не то, что я вот сейчас хотел, т.к. это всё же не solver а proover, но прикольно было потыкаться. Как solver тыкаю другое.

[1] Acorn https://acornprover.org/

#acorn #formal_methods #formalMethods

AI coding tools have become pretty impressive (my PhD student just used Claude Code to develop a checker for Hoare proofs that features a custom decision procedure in a single afternoon - from scratch).

At the same time, these tools "can introduce insidious bugs or other problems that are difficult to immediately identify and relatively time-consuming to troubleshoot".

I feel there'll be a lot of work for the formal methods research community 😉

#arstechnica #vibe_coding #formal_methods

arstechnica.com/ai/2025/07/developer-survey-shows-trust-in-ai-coding-tools-is-falling-as-usage-rises/

PhD Opportunities in Computer Science (Fully Funded)

R@ISE Project (University of Limerick)

See the full job description on jobRxiv: https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91424

#computer_science #formal_methods #model_driven_development #software_engineering #ScienceJobs #...
https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91424

Verified Effectful Programming in F* - Catalin Hritcu

https://infosec.pub/post/22390175

PhD Opportunities in Computer Science (Fully Funded)

R@ISE Project (University of Limerick)

See the full job description on jobRxiv: https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91060

#computer_science #formal_methods #model_driven_development #software_engineering #ScienceJobs #...
https://jobrxiv.org/job/rise-project-university-of-limerick-27778-phd-opportunities-in-computer-science-fully-funded/?feed_id=91060

A couple years back I was introduced to some of the folks at Galois, and they convinced me that formal methods can lower the cost of software development. Now I’m reading this post from @marcbrooker where he adds a bit of nuance that I think is helpful. I’ll summarize it this way: formal methods can lower the total cost to develop and maintain system-level software, where the requirements are stable and well-understood. If you’re designing a user-facing system and need to interatively respond to customer feedback—in other words, if your requirements are shifting and poorly understood—Agile remains the best choice.

https://brooker.co.za/blog/2024/04/17/formal

#formal_methods #softwareengineering #agile

Like 4 people favourited my post about Nix.

This is the height of viral fame for me.

Social media isn't bad when there's zero marketing budget, no anger/attention/algorithm bullshit.

Anyway, I'm trying to package this with Nix:
https://github.com/SamueleGerminiani/harm

I'm working through a CMake issue - the C++ can't find antlr4-runtime.h. Follow along for the gory details as I succeed or fail miserably!

#nix #nixos #cmake #formal_methods