I started looking at ACSL in Frama-C. Looks promising, although a bit complex at first.

I wonder if I can convey it to output its proofs in some readable format for archiving. And it would be swell with some test report or so. Perhaps also a non-zero return code so that it becomes more easily integrated in a regression test CI/CD pipeline.

#FramaC #ACSL

Leading Japanese Drone Maker ACSL Enters the U.S. Market

Can Japanese drone company ACSL take on the Chinese behemoth, DJI?

PetaPixel

The Anti-Capitalist Software License (#ACSL) can be adapted but as it stands does not require disclosure of derived code, instead limits use to individuals and organisations which do not exploit labour, but are either non-profit / educational, or employee owned.

https://anticapitalist.software/

Here's a good discussion of different open source #licensing in the context of #SafeNetwork, a quick way to get up to speed without the jargon or fine detail: https://safenetforum.org/t/protective-gpl-licences-vs-permissive-mit-bsd-licences/33724/18
#FOSS #GPL #MIT #BSD #Coop

The Anti-Capitalist Software License

A software license towards a world beyond capitalism.

エアロネクスト、極寒のモンゴル首都でドローン血液輸送--海外での飛行実証、初成功
https://japan.cnet.com/article/35211636/
#japan_cnet #ACSL #セイノーホールディングス #KDDI
エアロネクスト、極寒のモンゴル首都でドローン血液輸送--海外での飛行実証、初成功

エアロネクストは11月13日、モンゴル首都のウランバートル市において、ドローンで血液を輸送する実証実験を行った。

CNET Japan
ANA、国内2例目の「レベル4」ドローン配送--自社の「一等無人航空機操縦士」は国内初
https://japan.cnet.com/article/35211295/
#japan_cnet #ACSL #ANA #沖縄県
ANA、国内2例目の「レベル4」ドローン配送--自社の「一等無人航空機操縦士」は国内初

ANAホールディングスは11月8日、沖縄県久米島町において、「レベル4飛行」でのドローン配送サービスの実証実験の報道公開を行った。

CNET Japan
"The current verification tool for #ACSL is #FramaC. It also implements a sister language, ANSI/ISO C++ Specification Language (ACSL++), defined for C++."

https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language

last time I checked, C++ was left out, only C was supported — times have changed?

now I wonder where #Rust is in the process — there seems to be an ongoing work but nothing that would stand out yet

for #Ada there is #SPARK

https://en.wikipedia.org/wiki/SPARK_(programming_language)

and #PSL is actually independent from the HDLs, can be added on top of VHDL, SV, or Synthesizable #SystemC as well, though the implementations are uncertain

https://en.wikipedia.org/wiki/Property_Specification_Language

p.s. #Accelera good, IEEE bad
Stereophonic

@alys released under "The Anti-Capitalist Software License", very cool license!
>> https://anticapitalist.software
#ACSL #software #license #libre
The Anti-Capitalist Software License

A software license towards a world beyond capitalism.

@fede Llevo leídos varios mensajes sobre la #LicenciaAnticapitalista y hay un aspecto que me inquieta: Si el acceso al código fuente no es requisito indispensable para el software #acsl, ¿cómo evitar que desde "el sistema" cuelen código malicioso para, por ejemplo, extraer información de personas incómodas para "el sistema"? 🤔

#FramaC WP just threw at me that #ACSL lambdas are not supported yet. How the hell am i supposed to use \numof ?! #framacWP #formalmethods

I have time to figure it out till Dec30