{"guid":"9cb583b3-6cde-41cf-a68a-780fc88603eb","title":"Correct by Construction Concurrent Programs in Idris 2","subtitle":null,"slug":"bob11-2025-correct-by-construction-concurrent-programs-in-idris-allais","link":"https://bobkonf.de/2025/allais.html","description":"Concurrent programs destructively updating shared memory are notoriously hard to get right. Concurrent separation logics are logics with built-in notions of e.g. ownership of memory regions, concurrent accesses, and lock mechanisms. They give experts a way to verify a posteriori that complex concurrent imperative programs hopefully abide by their formal specification.\n          \n          We will see how next generation languages let us get rid of a posteriori verification in favour of a correct-by-construction approach whereby the program is interactively built in a specification-respecting dialogue with the compiler. For this presentation we will be using Idris 2, a general purpose functional language with an expressive type system combining dependent types to enforce complex invariants and linear logic to track resource usage.\n          \n          We will demonstrate how a simple library can capture ideas from concurrent separation logic by providing proof-carrying concurrent primitives. These make it impossible to write into memory one does not own or to release a lock without having proven that its associated invariant has been re-established. They also guarantee that whatever is read from the shared memory is invariant-respecting.\n          \n          This will culminate in worked out example e.g. the definition of map-reduce primitives repeatedly and safely breaking down a buffer into chunks that can be processed concurrently and/or a naïve bank with concurrent cash machines.\n\nLicensed to the public under https://creativecommons.org/licenses/by/3.0/de","original_language":"eng","persons":["Guillaume Allais"],"tags":["11","2025","bob2025","Talk","Talks #2","bob2025-eng","BOB","BOB Konferenz","Day 1"],"view_count":174,"promoted":false,"date":"2025-03-14T13:00:00.000+01:00","release_date":"2025-04-29T00:00:00.000+02:00","updated_at":"2026-03-21T14:00:07.838+01:00","length":2671,"duration":2671,"thumb_url":"https://static.media.ccc.de/media/events/bobkonf/2025/11-9cb583b3-6cde-41cf-a68a-780fc88603eb.jpg","poster_url":"https://static.media.ccc.de/media/events/bobkonf/2025/11-9cb583b3-6cde-41cf-a68a-780fc88603eb_preview.jpg","timeline_url":"https://static.media.ccc.de/media/events/bobkonf/2025/11-9cb583b3-6cde-41cf-a68a-780fc88603eb.timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/events/bobkonf/2025/11-9cb583b3-6cde-41cf-a68a-780fc88603eb.thumbnails.vtt","frontend_link":"https://media.ccc.de/v/bob11-2025-correct-by-construction-concurrent-programs-in-idris-allais","url":"https://api.media.ccc.de/public/events/9cb583b3-6cde-41cf-a68a-780fc88603eb","conference_title":"BOB Konferenz 2025","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2025","related":[],"recordings":[{"size":40,"length":2671,"mime_type":"audio/mpeg","language":"eng","filename":"bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_mp3.mp3","state":"new","folder":"mp3","high_quality":false,"width":0,"height":0,"updated_at":"2025-04-29T16:36:45.305+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2025/mp3/bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_mp3.mp3","url":"https://api.media.ccc.de/public/recordings/87415","event_url":"https://api.media.ccc.de/public/events/9cb583b3-6cde-41cf-a68a-780fc88603eb","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2025"},{"size":25,"length":2671,"mime_type":"audio/opus","language":"eng","filename":"bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_opus.opus","state":"new","folder":"opus","high_quality":false,"width":0,"height":0,"updated_at":"2025-04-29T16:36:07.648+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2025/opus/bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_opus.opus","url":"https://api.media.ccc.de/public/recordings/87414","event_url":"https://api.media.ccc.de/public/events/9cb583b3-6cde-41cf-a68a-780fc88603eb","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2025"},{"size":200,"length":2671,"mime_type":"video/webm","language":"eng","filename":"bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_webm-hd.webm","state":"new","folder":"webm-hd","high_quality":true,"width":2560,"height":1440,"updated_at":"2025-04-29T17:16:27.637+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2025/webm-hd/bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_webm-hd.webm","url":"https://api.media.ccc.de/public/recordings/87423","event_url":"https://api.media.ccc.de/public/events/9cb583b3-6cde-41cf-a68a-780fc88603eb","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2025"},{"size":72,"length":2671,"mime_type":"video/webm","language":"eng","filename":"bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_webm-sd.webm","state":"new","folder":"webm-sd","high_quality":false,"width":720,"height":576,"updated_at":"2025-04-29T17:04:58.357+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2025/webm-sd/bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_webm-sd.webm","url":"https://api.media.ccc.de/public/recordings/87420","event_url":"https://api.media.ccc.de/public/events/9cb583b3-6cde-41cf-a68a-780fc88603eb","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2025"},{"size":55,"length":2671,"mime_type":"video/mp4","language":"eng","filename":"bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_sd.mp4","state":"new","folder":"h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2025-04-29T16:39:18.340+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2025/h264-sd/bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_sd.mp4","url":"https://api.media.ccc.de/public/recordings/87416","event_url":"https://api.media.ccc.de/public/events/9cb583b3-6cde-41cf-a68a-780fc88603eb","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2025"},{"size":150,"length":2671,"mime_type":"video/mp4","language":"eng","filename":"bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_hd.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":2560,"height":1440,"updated_at":"2025-04-29T15:15:31.359+02:00","recording_url":"https://cdn.media.ccc.de/events/bobkonf/2025/h264-hd/bob2025-11-eng-Correct_by_Construction_Concurrent_Programs_in_Idris_2_hd.mp4","url":"https://api.media.ccc.de/public/recordings/87396","event_url":"https://api.media.ccc.de/public/events/9cb583b3-6cde-41cf-a68a-780fc88603eb","conference_url":"https://api.media.ccc.de/public/conferences/bobkonf2025"}]}