Logs: freenode/#haskell
| 2020-11-18 17:58:39 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 2020-11-18 17:58:40 | <p0a> | is there heap allocation in firmware? |
| 2020-11-18 17:58:42 | <texasmynsted> | s/the/then/ |
| 2020-11-18 17:58:43 | <maerwald> | that's not much to throw around "safe" |
| 2020-11-18 17:58:51 | <p0a> | I have never programmed anything like firmware, I don't even know what it is |
| 2020-11-18 17:58:52 | <merijn> | maerwald: Define "safe" |
| 2020-11-18 17:59:00 | <srk> | p0a: yup, ivory-tower uses heap for FreeRTOS tasks |
| 2020-11-18 17:59:06 | <merijn> | maerwald: Definitely safer than hand-written C |
| 2020-11-18 17:59:09 | <maerwald> | merijn: formally verified at least |
| 2020-11-18 17:59:11 | <merijn> | maerwald: Sure, that's not a high bar |
| 2020-11-18 17:59:27 | <merijn> | maerwald: It plugs into formal verification tools as possible backends, that's one of the points/goals :p |
| 2020-11-18 17:59:39 | <texasmynsted> | Example: I have written firmware to control the hardware in a water meter and let the water meter communicate over radio. |
| 2020-11-18 17:59:46 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-xcriusnvhpaknzlz) |
| 2020-11-18 17:59:51 | <merijn> | maerwald: Per the Ivory webpage: "The C language backend supports rendering Ivory assertions for static checking with the CBMC model checker. The SMACCMPilot project build system includes integration for CBMC verification of the SMACCMPilot source code." |
| 2020-11-18 17:59:55 | <merijn> | We also provide our own symbolic simulator for verifying Ivory assertions using CVC4. |
| 2020-11-18 18:00:09 | <texasmynsted> | I have written code for the head unit in automobiles |
| 2020-11-18 18:00:18 | <maerwald> | ok, you're all hired :p |
| 2020-11-18 18:00:18 | <p0a> | srk: I had no idea how 'large' firmware can be. I didn't know OSes run on them. I know very little about it :P |
| 2020-11-18 18:00:27 | <texasmynsted> | That is what I mean by firmware |
| 2020-11-18 18:00:37 | → | Klobbinger joins (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) |
| 2020-11-18 18:00:42 | × | motherfsck quits (~motherfsc@unaffiliated/motherfsck) (Remote host closed the connection) |
| 2020-11-18 18:00:51 | <merijn> | texasmynsted: Iirc Ivory was originally developed for crypto/firmware applications for DARPA/US Dept of Defense |
| 2020-11-18 18:01:24 | <merijn> | texasmynsted: So it's *very* much intended for stuff like "car firmware" |
| 2020-11-18 18:01:31 | <texasmynsted> | maerwald: Excellent. What are we building? |
| 2020-11-18 18:01:41 | × | Klobbinger quits (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) (Remote host closed the connection) |
| 2020-11-18 18:01:42 | <maerwald> | a stupid backend :D |
| 2020-11-18 18:01:50 | → | crdrost joins (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) |
| 2020-11-18 18:01:50 | <p0a> | nice! |
| 2020-11-18 18:01:53 | <merijn> | Oh, that's easy |
| 2020-11-18 18:01:57 | <merijn> | I've build tons of those |
| 2020-11-18 18:02:18 | <srk> | p0a: depends, I'm typically using STM32 MCUs ranging from 8kb to 512kb SRAM (64kb - 1/2Mb flash) |
| 2020-11-18 18:02:26 | <texasmynsted> | maerwald: More specifically please. That pretty much describes everything.] |
| 2020-11-18 18:02:45 | → | motherfsck joins (~motherfsc@unaffiliated/motherfsck) |
| 2020-11-18 18:02:47 | <maerwald> | I dunno... is there anything other than backends out there? |
| 2020-11-18 18:02:47 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 2020-11-18 18:02:54 | <merijn> | p0a: It depends on your chip too |
| 2020-11-18 18:03:12 | <monochrom> | merijn: Do you happen to know why they chose the name Ivory? Is it about "yes this is from the ivory power, bite me"? :) |
| 2020-11-18 18:03:15 | <merijn> | p0a: Embedded chips powerful enough to run regular linux or pretty cheap |
| 2020-11-18 18:03:21 | <merijn> | monochrom: Probably? |
| 2020-11-18 18:03:27 | <srk> | it's explained in one of the papers |
| 2020-11-18 18:03:43 | <merijn> | monochrom: Considering there's an associated language mentioned on their website called "tower"... |
| 2020-11-18 18:03:44 | <srk> | something like 'to bring embedded development down from ivory tower' |
| 2020-11-18 18:03:52 | <monochrom> | hahaha neat |
| 2020-11-18 18:03:58 | → | Klobbinger joins (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) |
| 2020-11-18 18:04:01 | → | brisbin joins (~patrick@pool-173-49-158-4.phlapa.fios.verizon.net) |
| 2020-11-18 18:04:03 | → | britva joins (~britva@31-10-157-156.cgn.dynamic.upc.ch) |
| 2020-11-18 18:04:04 | <monochrom> | thanks merijn and srk |
| 2020-11-18 18:04:25 | × | nut quits (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 2020-11-18 18:04:48 | <merijn> | monochrom: That's why the clash people had to figure out something else to name clash ;) |
| 2020-11-18 18:04:58 | <merijn> | (statement not actually based in facts) |
| 2020-11-18 18:05:08 | <monochrom> | hahahahaha name clash |
| 2020-11-18 18:05:55 | <texasmynsted> | Hmm. I would love to see people describe their experience with various commodity chips. |
| 2020-11-18 18:06:17 | <merijn> | I'm just sad Habit died |
| 2020-11-18 18:06:40 | <monochrom> | In other news, today I showed my students the fibonacci joke "This Fibonacci joke is as bad as the last two you heard combined." and the originating tweet URL https://twitter.com/sigfpe/status/776420034419658752 |
| 2020-11-18 18:06:46 | × | jakob_ quits (~textual@p200300f49f1622000c6d85cd02bcc449.dip0.t-ipconnect.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 2020-11-18 18:08:17 | <merijn> | heh, so according to reddit Haskell job openings it's "hard to find people with 5+ years experience", so clearly I need to start demanding rockstar salary by now >.> |
| 2020-11-18 18:09:04 | <Ariakenom> | texasmynsted: A colleague had an awesome patch for an avr8. It just rearranged members in a struct. |
| 2020-11-18 18:09:38 | <texasmynsted> | merijn: You should. |
| 2020-11-18 18:10:01 | <Ariakenom> | the compiled code was smaller because the members were in nicer locations. he find out where to place them by trying all of them in a script |
| 2020-11-18 18:10:12 | <texasmynsted> | Where do you work? |
| 2020-11-18 18:10:16 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:d849:743b:370b:b3cd) (Quit: cosimone) |
| 2020-11-18 18:10:41 | <Ariakenom> | we needed that because we were running out of flash storage on them |
| 2020-11-18 18:10:44 | <merijn> | texasmynsted: Well currently I don't write Haskell to begin with, or rather, at least not officially :p |
| 2020-11-18 18:10:52 | <texasmynsted> | What? |
| 2020-11-18 18:10:55 | <texasmynsted> | That is crazy |
| 2020-11-18 18:11:01 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 2020-11-18 18:11:03 | <texasmynsted> | What do you write? |
| 2020-11-18 18:11:37 | <maerwald> | IRC |
| 2020-11-18 18:11:42 | <texasmynsted> | So like many of us Haskell is your guilty pleasure? |
| 2020-11-18 18:11:42 | <maerwald> | look at his IRC stats |
| 2020-11-18 18:11:44 | <maerwald> | :p |
| 2020-11-18 18:11:45 | <merijn> | maerwald: shush |
| 2020-11-18 18:11:46 | <texasmynsted> | LOLOL |
| 2020-11-18 18:11:47 | → | conal joins (~conal@64.71.133.70) |
| 2020-11-18 18:11:51 | <p0a> | Ariakenom: can't you just pack a struct? |
| 2020-11-18 18:12:04 | <merijn> | maerwald: dminuoso is still in first because (thank god) Chris Done's ircbrowse stats got lost |
| 2020-11-18 18:12:23 | tomsmeding | . o O ( it will grow over time ) |
| 2020-11-18 18:12:28 | <texasmynsted> | I think you could argue you are promoting your haskell mentoring |
| 2020-11-18 18:12:39 | <Ariakenom> | p0a: it wasnt to reduce memory. it was to reduce code size :D |
| 2020-11-18 18:13:04 | <merijn> | texasmynsted: Currently C, C++, Fortran90, Python, within the organisation probably "basically everything besides, like, PHP and perl" :p |
| 2020-11-18 18:13:10 | <texasmynsted> | His handle must not be chrisdone |
| 2020-11-18 18:13:34 | <texasmynsted> | Fortran90. Interesting. |
| 2020-11-18 18:13:37 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 2020-11-18 18:13:50 | <merijn> | texasmynsted: That's for the lucky people not dealing with Fortran77 :p |
| 2020-11-18 18:14:11 | <p0a> | Ariakenom: I'm confused, but I believe you :) |
| 2020-11-18 18:14:20 | <texasmynsted> | I am trying to determine where you work where Fortran90 would be used. . . |
| 2020-11-18 18:14:32 | <merijn> | texasmynsted: Oh, I still write Haskell stuff at work, because no one's around to tell me no :p |
| 2020-11-18 18:16:32 | → | valdyn joins (~valdyn@host-88-217-143-53.customer.m-online.net) |
| 2020-11-18 18:16:35 | <texasmynsted> | Well it sound interesting |
| 2020-11-18 18:18:37 | <texasmynsted> | I like how some people say they use Haskell for "prototyping" |
| 2020-11-18 18:19:07 | × | knupfer quits (~Thunderbi@200116b8244bd600859a1b799407ebc4.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 2020-11-18 18:20:04 | <dolio> | Haskell is too mainstream for prototyping. |
| 2020-11-18 18:20:12 | <dolio> | Prototype your Haskell stuff in Agda. |
| 2020-11-18 18:20:33 | <texasmynsted> | or Idris |
| 2020-11-18 18:20:57 | <dolio> | Yeah. Although if you prototype in Idris you might find you can just use the prototype. :þ |
| 2020-11-18 18:21:35 | <texasmynsted> | yes. That is the point. A Haskell prototype likely works better and is more maintainable than the target language |
| 2020-11-18 18:21:55 | → | jedai42 joins (~jedai@lfbn-dij-1-708-251.w90-100.abo.wanadoo.fr) |
| 2020-11-18 18:22:00 | <monochrom> | Programmers seldom grow out of their prototypes. |
| 2020-11-18 18:22:09 | <merijn> | Prototype in Haskell, because we all know prototypes become production and never stop, so now they gotta hire more haskellers to support it |
| 2020-11-18 18:22:14 | <merijn> | Boom. Haskell shop |
All times are in UTC.